attempt to solve issue #131

share/provers-detection-data.conf

@@ -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.

src/driver/call_provers.ml

@@ -364,8 +364,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 }