Commit 74206b7d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix timeout detection for Z3.

Option -t is in milliseconds, while option -T is in second.
parent 25b8bc71
...@@ -395,7 +395,7 @@ version_ok = "4.5.0" ...@@ -395,7 +395,7 @@ version_ok = "4.5.0"
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"
command = "%e -smt2 -T:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command = "%e -smt2 -T:%t 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"
use_at_auto_level = 1 use_at_auto_level = 1
...@@ -415,7 +415,7 @@ version_ok = "4.5.0" ...@@ -415,7 +415,7 @@ version_ok = "4.5.0"
version_old = "4.4.1" version_old = "4.4.1"
version_old = "4.4.0" version_old = "4.4.0"
driver = "z3_432" driver = "z3_432"
command = "%e -smt2 -T:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command = "%e -smt2 -T:%t 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.3.2 does not support option global option -rs anymore. # Z3 4.3.2 does not support option global option -rs anymore.
......
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