changeset 41130 | 130771a48c70 |
parent 41127 | 2ea84c8535c6 |
child 41235 | 975db7bd23e3 |
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed Dec 15 10:12:48 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed Dec 15 10:12:48 2010 +0100 @@ -66,7 +66,7 @@ fun z3_options ctxt = ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), - "MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"] + "MODEL=true", "-smt"] |> not (Config.get ctxt SMT_Config.oracle) ? append ["DISPLAY_PROOF=true","PROOF_MODE=2"]