# HG changeset patch
# User blanchet
# Date 1506098771 10800
# Node ID fdab65297bd6fc32ee1e63a5e0229e20124e305e
# Parent  bc3584f7ac0c2e590376998eddb496214f860614
real oracle

diff -r bc3584f7ac0c -r fdab65297bd6 NEWS
--- a/NEWS	Tue Sep 19 16:37:19 2017 +0100
+++ b/NEWS	Fri Sep 22 13:46:11 2017 -0300
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* SMT module:
+  - The 'smt_oracle' option is now necessary when using the 'smt' method
+    with a solver other than Z3.
+
 
 New in Isabelle2017 (October 2017)
 ----------------------------------
diff -r bc3584f7ac0c -r fdab65297bd6 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Sep 19 16:37:19 2017 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 22 13:46:11 2017 -0300
@@ -202,9 +202,13 @@
       (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output =
     (case outcome output of
       (Unsat, lines) =>
-        if not (Config.get ctxt SMT_Config.oracle) andalso is_some replay0
-        then the replay0 outer_ctxt replay_data lines
-        else oracle ()
+        if Config.get ctxt SMT_Config.oracle then
+          oracle ()
+        else
+          (case replay0 of
+            SOME replay => replay outer_ctxt replay_data lines
+          | NONE => error "No proof reconstruction for solver -- \
+            \declare [[smt_oracle]] to allow oracle")
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   val cfalse = Thm.cterm_of @{context} @{prop False}