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/run-script-smtcomp2015-application | |
| 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/run-script-smtcomp2015-application')
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application | 4 |
1 files changed, 2 insertions, 2 deletions
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 |