src/HOL/Tools/SMT2/smt2_systems.ML
changeset 57168 af95a414136a
parent 57164 eb5f27ec3987
child 57209 7ffa0f7e2775
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 14:38:41 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 16:02:41 2014 +0200
@@ -125,6 +125,7 @@
 
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+     "smt.refine_inj_axioms=false",
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
      "-smt2"]