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

diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
index 9b8a0ba389d2413adf4f30a76558a7f3a9dde8d5..3602eb57616a2662a7e21c62d8d2a56f5be28cca 100755 (executable)
--- 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 4219241ef352006f3cb583e1fab20bc6ca152301..b3149ce7cd2587e5b978d0e2620ccbcb11f7d793 100755 (executable)
--- 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