src/HOL/Tools/SMT/smt_setup_solvers.ML
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"]