diff --git a/drivers/z3_440.drv b/drivers/z3_440.drv index 984bc3cb0a3820f813eaaa5a13a39a09dfcfdca1..f408b85f97a4260c56aa8198dfd0c99cdf95d3cd 100644 --- a/drivers/z3_440.drv +++ b/drivers/z3_440.drv @@ -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 diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index c886712ac7996304903a1637f7dcbcda3ebb6dde..94940133871cd9eb5763b1918bf13147de4212e5 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -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"