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"]