diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-12 17:21:38 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-12 17:21:38 -0400 |
| commit | 129bc08026341f4876c761fa5b10c23205e20a57 (patch) | |
| tree | b0ed9346931c9644ca27c58d53dea7080f24a1f9 /contrib/run-script-smtcomp2015-assertions | |
| parent | 8e83c475f6def7fc33131f67ee5b7e28ddf8a2cc (diff) | |
sync options of default-assertions run script with default
Diffstat (limited to 'contrib/run-script-smtcomp2015-assertions')
| -rwxr-xr-x | contrib/run-script-smtcomp2015-assertions | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions index b364cc07c..4fa96af71 100755 --- a/contrib/run-script-smtcomp2015-assertions +++ b/contrib/run-script-smtcomp2015-assertions @@ -1,11 +1,11 @@ #!/bin/bash +cvc4=./cvc4-assertions # Attempt to run each benchmark 1-5 min depending on numconfigs # quanitifers get 5 min / benchmark # quantifier free uf, arith, arrays get 1 min / benchmark # qf_bv gets 1 min wall (2 min user) / benchmark -cvc4=./cvc4-assertions bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') @@ -59,7 +59,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) trywith 10 --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 10 --finite-model-find --mbqi=gen-ev --uf-ss-totality trywith 10 --inst-when=full --full-saturate-quant - trywith 10 --fmf-bound-int --macros-quant + #trywith 10 --fmf-bound-int --macros-quant # recently bug fixed trywith 10 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 10 --decision=justification-stoponly --full-saturate-quant # large runs 3min @@ -67,7 +67,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) trywith 10 --finite-model-find --mbqi=none trywith 10 --decision=internal --full-saturate-quant # last call runs 20min - trywith 20 --finite-model-find --fmf-inst-engine --quant-cf --sort-inference --uf-ss-fair + trywith 20 --finite-model-find --fmf-inst-engine --quant-cf --sort-inference --uf-ss-fair trywith 20 --no-inst-no-entail --full-saturate-quant finishwith --full-saturate-quant ;; |