Commit 25b8bc71 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' of gitlab.inria.fr:why3/why3

parents bf5118ff 88f7c204
......@@ -71,7 +71,7 @@ version_ok = "1.5"
driver = "cvc4_15"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command = "%e --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1
......@@ -88,7 +88,7 @@ driver = "cvc4_14"
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command = "%e --tlimit=%t000 --lang=smt2 %f"
use_at_auto_level = 1
# CVC4 version 1.4, not using SMTLIB bitvectors
......@@ -105,7 +105,7 @@ driver = "cvc4"
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command = "%e --tlimit=%t000 --lang=smt2 %f"
# CVC4 version 1.0 to 1.3
......@@ -376,6 +376,7 @@ version_ok = "4.5.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_440_counterexample"
# -t sets the time limit per query
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"
......@@ -394,7 +395,7 @@ version_ok = "4.5.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_440"
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"
use_at_auto_level = 1
......@@ -414,7 +415,7 @@ version_ok = "4.5.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_432"
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"
# Z3 4.3.2 does not support option global option -rs anymore.
......
......@@ -368,8 +368,8 @@ let adapt_limits limit on_timelimit =
(* for steps limit use 2 * t + 1 time *)
if limit.limit_steps <> empty_limit.limit_steps
then (2 * limit.limit_time + 1)
(* if prover implements time limit, use 16t + 1 *)
else if on_timelimit then 16 * limit.limit_time + 1
(* if prover implements time limit, use 4t + 1 *)
else if on_timelimit then 4 * limit.limit_time + 1
(* otherwise use t *)
else limit.limit_time }
......
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