From 04b5831c54503bd856b69777b1fefab19d925ac1 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 30 May 2014 14:38:05 -0400
Subject: [PATCH] run script fix

---
 contrib/run-script-smtcomp2014 | 42 +++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index b121c6956..5ba3506cd 100755
--- 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)
-- 
2.30.2