run script fix

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index b121c69569c9b71a3148d5a2dd81210d39e41501..5ba3506cdc25b757db1985a1f6c94c93e125b351 100755 (executable)
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -30,33 +30,33 @@ QF_LRA)
 AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA)
   # the following is designed for a run time of 1500s.
   # initial runs
-  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
+  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
   # more runs...
-  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
+  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
   # medium runs (2 min per)
-  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
+  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
   # last call runs (5 min per)
-  trywith 300 --full-saturate-quant
-  trywith 300 --finite-model-find --sort-inference --uf-ss-fair 
+  trywith --time-limit-per=300000 --full-saturate-quant
+  trywith --time-limit-per=300000 --finite-model-find --sort-inference --uf-ss-fair 
   finishwith --quant-cf --full-saturate-quant
   ;;
 LRA)
-  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
+  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
   finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
   ;;
 QF_AUFBV)