sync exerimental scripts with regular ones

diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental
index 69b3f8b37c765ea8672ab816503975a7b2b80c66..4219241ef352006f3cb583e1fab20bc6ca152301 100755 (executable)
--- 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 3fc8ccec5bc45cd09a28464b1faeb8d317752520..9b8a0ba389d2413adf4f30a76558a7f3a9dde8d5 100755 (executable)
--- 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