Commit a3751678 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'diff_drivers' into 'master'

Add comment prelude and outofmemory error for z3 driver

See merge request !121
parents 841170c6 a8b06f74
(** Why3 driver for Z3 <= 4.3.1 *) (** Why3 driver for Z3 <= 4.3.1 *)
prelude ";; produced by z3.drv ;;"
prelude "(set-logic AUFNIRA)" prelude "(set-logic AUFNIRA)"
(* A : Array (* A : Array
UF : Uninterpreted Function UF : Uninterpreted Function
...@@ -27,6 +28,7 @@ transformation "encoding_smt" ...@@ -27,6 +28,7 @@ transformation "encoding_smt"
(** Error messages specific to Z3 *) (** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory" outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
steplimitexceeded "Maximal allocation counts .* have been exceeded\\|(error \".*number of configured allocations exceeded\")"
timeout "interrupted by timeout" timeout "interrupted by timeout"
(* stop reporting Z3 2.19 warnings as errors *) (* stop reporting Z3 2.19 warnings as errors *)
fail "^(error \"\\(\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\).*\\)\")" "Error: \\1" fail "^(error \"\\(\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\).*\\)\")" "Error: \\1"
......
...@@ -4,6 +4,8 @@ ...@@ -4,6 +4,8 @@
prelude "(set-logic AUFNIRA)" prelude "(set-logic AUFNIRA)"
*) *)
prelude ";; produced by z3_432.drv ;;"
(* Counterexamples: set model parser *) (* Counterexamples: set model parser *)
model_parser "smtv2" model_parser "smtv2"
...@@ -41,6 +43,7 @@ transformation "encoding_smt_if_poly" ...@@ -41,6 +43,7 @@ transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *) (** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory" outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
steplimitexceeded "Maximal allocation counts .* have been exceeded\\|(error \".*number of configured allocations exceeded\")"
timeout "interrupted by timeout" timeout "interrupted by timeout"
(** Extra theories supported by Z3 *) (** Extra theories supported by Z3 *)
......
...@@ -44,6 +44,7 @@ transformation "encoding_smt_if_poly" ...@@ -44,6 +44,7 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory" outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout" timeout "interrupted by timeout"
steps ":rlimit-count +\\([0-9]+\\)" 1
(** Z3 needs "(push)" to provide models *) (** Z3 needs "(push)" to provide models *)
theory BuiltIn theory BuiltIn
......
...@@ -393,7 +393,7 @@ driver = "z3_440_counterexample" ...@@ -393,7 +393,7 @@ driver = "z3_440_counterexample"
command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 >= 4.4.0, with BV support # Z3 >= 4.5.0, with BV support
[ATP z3] [ATP z3]
name = "Z3" name = "Z3"
exec = "z3" exec = "z3"
...@@ -403,8 +403,6 @@ exec = "z3-4.8.1" ...@@ -403,8 +403,6 @@ exec = "z3-4.8.1"
exec = "z3-4.7.1" exec = "z3-4.7.1"
exec = "z3-4.6.0" exec = "z3-4.6.0"
exec = "z3-4.5.0" exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version" version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)" version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.8.4" version_ok = "4.8.4"
...@@ -413,6 +411,19 @@ version_ok = "4.8.1" ...@@ -413,6 +411,19 @@ version_ok = "4.8.1"
version_ok = "4.7.1" version_ok = "4.7.1"
version_ok = "4.6.0" version_ok = "4.6.0"
version_ok = "4.5.0" version_ok = "4.5.0"
driver = "z3_440"
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
use_at_auto_level = 1
# Z3 = 4.4.0, with BV support
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_old = "4.4.1" version_old = "4.4.1"
version_old = "4.4.0" version_old = "4.4.0"
driver = "z3_440" driver = "z3_440"
......
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