Change SMT COMP script to use external timeouts.

1 files changed, 28 insertions, 27 deletions

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index a4737142a..2b22b9727 100755
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -10,7 +10,8 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # which case this run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
-  result="$($cvc4 -L smt2 --no-checking --no-interactive "$@" $bench)"
+  limit=$1; shift;
+  result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-checking --no-interactive "$@" $bench)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
   esac
@@ -30,47 +31,47 @@ QF_LRA)
 AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA)
   # the following is designed for a run time of 1500s.
   # initial runs
-  trywith --time-limit-per=20000 --simplification=none --decision=internal --full-saturate-quant
-  trywith --time-limit-per=20000 --quant-cf --pre-skolem-quant --full-saturate-quant
-  trywith --time-limit-per=20000 --finite-model-find --mbqi=none
+  trywith 20 --simplification=none --decision=internal --full-saturate-quant
+  trywith 20 --quant-cf --pre-skolem-quant --full-saturate-quant
+  trywith 20 --finite-model-find --mbqi=none
   # more runs...
-  trywith --time-limit-per=30000 --relevant-triggers --full-saturate-quant
-  trywith --time-limit-per=30000 --quant-cf --qcf-tconstraint --inst-when=last-call --full-saturate-quant
-  trywith --time-limit-per=30000 --finite-model-find --mbqi=gen-ev --uf-ss-totality
-  trywith --time-limit-per=30000 --disable-prenex-quant --full-saturate-quant
-  trywith --time-limit-per=20000 --simplification=none --decision=internal --pre-skolem-quant --full-saturate-quant
-  trywith --time-limit-per=20000 --quant-cf --quant-cf-mode=conflict --full-saturate-quant
-  trywith --time-limit-per=20000 --fmf-bound-int --macros-quant
+  trywith 30 --relevant-triggers --full-saturate-quant
+  trywith 30 --quant-cf --qcf-tconstraint --inst-when=last-call --full-saturate-quant
+  trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality
+  trywith 30 --disable-prenex-quant --full-saturate-quant
+  trywith 20 --simplification=none --decision=internal --pre-skolem-quant --full-saturate-quant
+  trywith 20 --quant-cf --quant-cf-mode=conflict --full-saturate-quant
+  trywith 20 --fmf-bound-int --macros-quant
   # medium runs (2 min per)
-  trywith --time-limit-per=120000 --decision=justification-stoponly --full-saturate-quant
-  trywith --time-limit-per=120000 --quant-cf --qcf-tconstraint --full-saturate-quant
-  trywith --time-limit-per=120000 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
+  trywith 120 --decision=justification-stoponly --full-saturate-quant
+  trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant
+  trywith 120 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
   # last call runs (5 min per)
-  trywith --time-limit-per=300000 --full-saturate-quant
-  trywith --time-limit-per=300000 --finite-model-find --sort-inference --uf-ss-fair 
+  trywith 300 --full-saturate-quant
+  trywith 300 --finite-model-find --sort-inference --uf-ss-fair 
   finishwith --quant-cf --full-saturate-quant
   ;;
 LRA)
-  trywith --time-limit-per=20000 --enable-cbqi --full-saturate-quant
-  trywith --time-limit-per=20000 --full-saturate-quant
-  trywith --time-limit-per=20000 --cbqi-recurse --full-saturate-quant
-  trywith --time-limit-per=30000 --quant-cf --full-saturate-quant
-  trywith --time-limit-per=60000 --quant-cf --qcf-tconstraint --full-saturate-quant
-  trywith --time-limit-per=120000 --cbqi-recurse --disable-prenex-quant --full-saturate-quant
+  trywith 20 --enable-cbqi --full-saturate-quant
+  trywith 20 --full-saturate-quant
+  trywith 20 --cbqi-recurse --full-saturate-quant
+  trywith 30 --quant-cf --full-saturate-quant
+  trywith 60 --quant-cf --qcf-tconstraint --full-saturate-quant
+  trywith 120 --cbqi-recurse --disable-prenex-quant --full-saturate-quant
   finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
   ;;
 QF_AUFBV)
-  trywith --tlimit-per=600000
+  trywith 600
   finishwith --decision=justification-stoponly
   ;;
 QF_BV)
-  trywith --bv-core --decision=justification --tlimit-per=10000
-  trywith --decision=justification --tlimit-per=60000
-  trywith --decision=internal --bitblast-eager --tlimit-per=600000
+  trywith 10 --bv-core --decision=justification
+  trywith 60 --decision=justification
+  trywith 600 --decision=internal --bitblast-eager
   finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
   ;;
 QF_AX)
-  trywith --tlimit-per=2000
+  trywith 2
   finishwith --no-arrays-model-based
   ;;
 *)