--- a/src/HOL/SMT.thy Tue Nov 10 14:43:29 2015 +0000
+++ b/src/HOL/SMT.thy Tue Nov 10 17:49:54 2015 +0100
@@ -2,7 +2,7 @@
Author: Sascha Boehme, TU Muenchen
*)
-section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
+section \<open>Bi ndings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
theory SMT
imports Divides
--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Nov 10 14:43:29 2015 +0000
+++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Nov 10 17:49:54 2015 +0100
@@ -109,7 +109,7 @@
smt_options = [(":produce-proofs", "true")],
default_max_relevant = 200 (* FUDGE *),
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
- "warning : proof_done: status is still open"),
+ "(error \"status is not unsat.\")"),
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }
--- a/src/HOL/Tools/SMT/verit_proof.ML Tue Nov 10 14:43:29 2015 +0000
+++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Nov 10 17:49:54 2015 +0100
@@ -118,9 +118,12 @@
let
fun mk_prop_of_term concl =
concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
+ fun update_prems assumption_id prems =
+ map (fn prem => id_of_father_step ^ prem)
+ (filter_out (curry (op =) assumption_id) prems)
fun inline_assumption assumption assumption_id
- (node as VeriT_Node {id, rule, prems, concl, bounds}) =
- mk_node id rule (filter_out (curry (op =) assumption_id) prems)
+ (VeriT_Node {id, rule, prems, concl, bounds}) =
+ mk_node id rule (update_prems assumption_id prems)
(@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
fun find_input_steps_and_inline [] last_step = ([], last_step)
| find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)