diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-04 08:14:30 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-04 08:14:36 +0200 |
| commit | 32cda667fac11b1768ed75d930cb5b0e6933ffe5 (patch) | |
| tree | 909ec2de9ee931f56a84dfbe68ebc110f0a95a61 /contrib | |
| parent | 0fde4ed8bcaa5dabd92ba9079455ca12df9ba2ec (diff) | |
Minor changes to smt comp script for quantified arith. Add option --cbqi-sat whether to disable sat for quantified arith.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2015 | 12 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index 3fc8ccec5..9b8a0ba38 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -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 diff --git a/contrib/run-script-smtcomp2015-application b/contrib/run-script-smtcomp2015-application index 69b3f8b37..4219241ef 100755 --- a/contrib/run-script-smtcomp2015-application +++ b/contrib/run-script-smtcomp2015-application @@ -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 |