Commit a8b06f74 authored by Sylvain Dailler's avatar Sylvain Dailler

Support rlimit for z3

This replace memory_max_alloc_count with rlimit.
parent f7290321
......@@ -44,6 +44,7 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps ":rlimit-count +\\([0-9]+\\)" 1
(** Z3 needs "(push)" to provide models *)
theory BuiltIn
......
......@@ -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_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]
name = "Z3"
exec = "z3"
......@@ -403,8 +403,6 @@ exec = "z3-4.8.1"
exec = "z3-4.7.1"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.8.4"
......@@ -413,6 +411,19 @@ version_ok = "4.8.1"
version_ok = "4.7.1"
version_ok = "4.6.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.0"
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