From 1a73025140a4f5dfc390d5ca462ce358b6f97f1b Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 4 Jun 2015 13:24:42 -0400 Subject: [PATCH] rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application} --- contrib/run-script-smtcomp2015 | 8 ++++---- 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 -- 2.30.2