# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1447174194 -3600
# Node ID a9c0572109af6a351062abb593edf2e25388e00a
# Parent  4f54d2759a0bd90e8aa1b555296a6f77a834357c
fixing premises in veriT proof reconstruction

diff -r 4f54d2759a0b -r a9c0572109af src/HOL/SMT.thy
--- 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
diff -r 4f54d2759a0b -r a9c0572109af src/HOL/Tools/SMT/smt_systems.ML
--- 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 }
 
diff -r 4f54d2759a0b -r a9c0572109af src/HOL/Tools/SMT/verit_proof.ML
--- 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)