diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-04 13:24:42 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-04 13:24:42 -0400 |
| commit | 1a73025140a4f5dfc390d5ca462ce358b6f97f1b (patch) | |
| tree | 8d8e8477e00420ada872e9f8f4e51e2cd62f5a17 /contrib | |
| parent | 35bf803bdc9a915d0270c3ce5b59aeb754d3351d (diff) | |
rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2015 | 8 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index 9b8a0ba38..3602eb576 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 60 --cbqi --full-saturate-quant + trywith 60 --cbqi --no-cbqi-sat --full-saturate-quant trywith 60 --full-saturate-quant - trywith 60 --cbqi --cbqi-recurse --full-saturate-quant + trywith 60 --cbqi --no-cbqi-sat --cbqi --no-cbqi-sat-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 + trywith 240 --cbqi --no-cbqi-sat --cbqi --no-cbqi-sat-recurse --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi --no-cbqi-sat-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 4219241ef..b3149ce7c 100755 --- a/contrib/run-script-smtcomp2015-application +++ b/contrib/run-script-smtcomp2015-application @@ -36,7 +36,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) runcvc4 ;; LIA|LRA|NIA|NRA) - runcvc4 --cbqi + runcvc4 --cbqi --no-cbqi-sat ;; QF_BV) runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 |