diff options
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 |