real oracle
authorblanchet
Fri Sep 22 13:46:11 2017 -0300 (20 months ago)
changeset 66661fdab65297bd6
parent 66660 bc3584f7ac0c
child 66662 4b10fa05423b
real oracle
NEWS
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/NEWS	Tue Sep 19 16:37:19 2017 +0100
     1.2 +++ b/NEWS	Fri Sep 22 13:46:11 2017 -0300
     1.3 @@ -7,6 +7,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* SMT module:
    1.10 +  - The 'smt_oracle' option is now necessary when using the 'smt' method
    1.11 +    with a solver other than Z3.
    1.12 +
    1.13  
    1.14  New in Isabelle2017 (October 2017)
    1.15  ----------------------------------
     2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Sep 19 16:37:19 2017 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 22 13:46:11 2017 -0300
     2.3 @@ -202,9 +202,13 @@
     2.4        (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output =
     2.5      (case outcome output of
     2.6        (Unsat, lines) =>
     2.7 -        if not (Config.get ctxt SMT_Config.oracle) andalso is_some replay0
     2.8 -        then the replay0 outer_ctxt replay_data lines
     2.9 -        else oracle ()
    2.10 +        if Config.get ctxt SMT_Config.oracle then
    2.11 +          oracle ()
    2.12 +        else
    2.13 +          (case replay0 of
    2.14 +            SOME replay => replay outer_ctxt replay_data lines
    2.15 +          | NONE => error "No proof reconstruction for solver -- \
    2.16 +            \declare [[smt_oracle]] to allow oracle")
    2.17      | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
    2.18  
    2.19    val cfalse = Thm.cterm_of @{context} @{prop False}