diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-30 14:38:05 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-30 14:38:05 -0400 |
| commit | 04b5831c54503bd856b69777b1fefab19d925ac1 (patch) | |
| tree | 6dd2f6af0b8c654d6fcf95b5beae3a9329a84911 /contrib | |
| parent | 73f533efbd887bae36a63a21bc531d412866e5a6 (diff) | |
run script fix
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2014 | 42 |
1 files 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) |