From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 4 Jun 2015 17:18:12 +0000 (-0400)
Subject: sync exerimental scripts with regular ones
X-Git-Tag: cvc5-1.0.0~6310
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35bf803bdc9a915d0270c3ce5b59aeb754d3351d;p=cvc5.git

sync exerimental scripts with regular ones
---

diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental
index 69b3f8b37..4219241ef 100755
--- a/contrib/run-script-smtcomp2015-application-experimental
+++ b/contrib/run-script-smtcomp2015-application-experimental
@@ -33,10 +33,10 @@ QF_LIA)
   runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites
   ;;
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
-  runcvc4 --simplification=none --decision=internal --full-saturate-quant
+  runcvc4 
   ;;
 LIA|LRA|NIA|NRA)
-  runcvc4 --enable-cbqi --full-saturate-quant
+  runcvc4 --cbqi
   ;;
 QF_BV)
   runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental
index 3fc8ccec5..9b8a0ba38 100755
--- a/contrib/run-script-smtcomp2015-experimental
+++ b/contrib/run-script-smtcomp2015-experimental
@@ -67,12 +67,12 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 20 --cbqi --full-saturate-quant
-  trywith 20 --full-saturate-quant
-  trywith 20 --cbqi --cbqi-recurse --full-saturate-quant
-  trywith 60 --qcf-tconstraint --full-saturate-quant
-  trywith 120 --cbqi --cbqi-recurse --full-saturate-quant
-  finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
+  trywith 60 --cbqi --full-saturate-quant
+  trywith 60 --full-saturate-quant
+  trywith 60 --cbqi --cbqi-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
   ;;
 QF_AUFBV)
   trywith 600