equal
deleted
inserted
replaced
123 local |
123 local |
124 fun z3_make_command name () = if_z3_non_commercial (make_command name) |
124 fun z3_make_command name () = if_z3_non_commercial (make_command name) |
125 |
125 |
126 fun z3_options ctxt = |
126 fun z3_options ctxt = |
127 ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
127 ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
|
128 "smt.refine_inj_axioms=false", |
128 "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), |
129 "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), |
129 "-smt2"] |
130 "-smt2"] |
130 |
131 |
131 fun select_class ctxt = |
132 fun select_class ctxt = |
132 if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C |
133 if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C |