Commit 273f4bde authored by Clément Fumex's avatar Clément Fumex

z3 > 4.3.1 don't have a specific logic set, it will choose by itself

parent 41ea4230
prelude "(set-logic AUFNIRA)"
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
import "z3_bare.drv"
import "discrimination.gen"
prelude "(set-logic AUFNIRA)"
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
(* div/mod of Z3 seems to be Euclidean Division *)
......@@ -26,3 +19,5 @@ theory real.FromInt
remove prop Mul
remove prop Neg
end
import "discrimination.gen"
\ No newline at end of file
......@@ -308,7 +308,7 @@ version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.3"
version_old = "4.3.2"
driver = "drivers/z3.drv"
driver = "drivers/z3_bare.drv" # Do not set any logic, let z3 choose by itself
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
[ATP z3]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment