--- 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)
----------------------------------
--- 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}