diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-04 13:18:12 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-04 13:18:12 -0400 |
| commit | 35bf803bdc9a915d0270c3ce5b59aeb754d3351d (patch) | |
| tree | aaaea9577762b8650d786aef6adede8edb4633a7 /contrib | |
| parent | 32cda667fac11b1768ed75d930cb5b0e6933ffe5 (diff) | |
sync exerimental scripts with regular ones
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application-experimental | 4 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-experimental | 12 |
2 files changed, 8 insertions, 8 deletions
diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental index 69b3f8b37..4219241ef 100755 --- a/contrib/run-script-smtcomp2015-application-experimental +++ b/contrib/run-script-smtcomp2015-application-experimental @@ -33,10 +33,10 @@ QF_LIA) runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites ;; ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) - runcvc4 --simplification=none --decision=internal --full-saturate-quant + runcvc4 ;; LIA|LRA|NIA|NRA) - runcvc4 --enable-cbqi --full-saturate-quant + runcvc4 --cbqi ;; QF_BV) runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental index 3fc8ccec5..9b8a0ba38 100755 --- a/contrib/run-script-smtcomp2015-experimental +++ b/contrib/run-script-smtcomp2015-experimental @@ -67,12 +67,12 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 20 --cbqi --full-saturate-quant - trywith 20 --full-saturate-quant - trywith 20 --cbqi --cbqi-recurse --full-saturate-quant - trywith 60 --qcf-tconstraint --full-saturate-quant - trywith 120 --cbqi --cbqi-recurse --full-saturate-quant - finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant + trywith 60 --cbqi --full-saturate-quant + trywith 60 --full-saturate-quant + trywith 60 --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --qcf-tconstraint --full-saturate-quant + trywith 240 --cbqi --cbqi-recurse --full-saturate-quant + finishwith --cbqi --cbqi-recurse --pre-skolem-quant --full-saturate-quant ;; QF_AUFBV) trywith 600 |