From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 27 May 2018 18:39:36 +0000 (-0700)
Subject: Fix no-cbqi-innermost option name in run script (#1994)
X-Git-Tag: cvc5-1.0.0~5004
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97914ba14805c6e6d84e45f33b3eea711a1e01a5;p=cvc5.git

Fix no-cbqi-innermost option name in run script (#1994)
---

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 5264bc26c..9057282e5 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -85,21 +85,21 @@ UFBV)
   # most problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant --decision=internal
   trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 30 --full-saturate-quant --cbqi-no-innermost --global-negate
+  trywith 30 --full-saturate-quant --no-cbqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 BV)
   trywith 120 --full-saturate-quant
-  trywith 120 --full-saturate-quant --cbqi-no-innermost
+  trywith 120 --full-saturate-quant --no-cbqi-innermost
   trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal
   trywith 30 --full-saturate-quant --no-cbqi-bv
   trywith 30 --full-saturate-quant --cbqi-bv-ineq=eq-slack
   # finish 10min
-  finishwith --full-saturate-quant --cbqi-no-innermost --global-negate
+  finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
   ;;
 LIA|LRA|NIA|NRA)
   trywith 30 --full-saturate-quant --nl-ext-tplanes
-  trywith 300 --full-saturate-quant --cbqi-no-innermost
+  trywith 300 --full-saturate-quant --no-cbqi-innermost
   trywith 300 --full-saturate-quant --cbqi-nested-qe
   finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;