From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 4 Jun 2015 17:24:42 +0000 (-0400)
Subject: rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}
X-Git-Tag: cvc5-1.0.0~6309
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a73025140a4f5dfc390d5ca462ce358b6f97f1b;p=cvc5.git

rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}
---

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