Commit f7290321 authored by Sylvain Dailler's avatar Sylvain Dailler

Add comment prelude and outofmemory error for z3 driver

parent c31bab2f
(** Why3 driver for Z3 <= 4.3.1 *)
prelude ";; produced by z3.drv ;;"
prelude "(set-logic AUFNIRA)"
(* A : Array
UF : Uninterpreted Function
......@@ -27,6 +28,7 @@ transformation "encoding_smt"
(** Error messages specific to Z3 *)
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"
(* 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"
......
......@@ -4,6 +4,8 @@
prelude "(set-logic AUFNIRA)"
*)
prelude ";; produced by z3_432.drv ;;"
(* Counterexamples: set model parser *)
model_parser "smtv2"
......@@ -41,6 +43,7 @@ transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
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"
(** Extra theories supported by 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