--- a/src/HOL/Tools/SMT2/smt2_systems.ML Fri Apr 25 22:13:17 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Fri Apr 25 22:13:17 2014 +0200
@@ -127,8 +127,7 @@
fun z3_make_command name () = if_z3_non_commercial (make_command name)
fun z3_options ctxt =
- ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
- "smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+ ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
"-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
"-smt2"]