--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu May 01 22:56:59 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu May 01 22:57:34 2014 +0200
@@ -182,7 +182,10 @@
((iidths, steps), TrueI)
else
let
- val ctxt4 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 []) ctxt3
+ val ctxt4 =
+ ctxt3
+ |> put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 [])
+ |> Config.put SAT.solver (Config.get ctxt3 SMT2_Config.sat_solver)
val proofs = fold (replay_step ctxt4 assumed) steps assumed
val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
val thm = Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4