From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 3 Jun 2017 18:27:52 +0000 (-0500)
Subject: Minor to smt comp script.
X-Git-Tag: cvc5-1.0.0~5778
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4e5b3250f6aaa82525aa7f5afa8de3086e2c5ee;p=cvc5.git

Minor to smt comp script.
---

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index ffa54bec9..9e351d58e 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -63,6 +63,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF
   trywith 30 --inst-when=full --full-saturate-quant
   trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
   trywith 30 --nl-ext --full-saturate-quant
+  trywith 30 --full-saturate-quant --quant-ind
   trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   # finite model find 2min
   trywith 20 --finite-model-find --mbqi=none
@@ -83,11 +84,13 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF
 UFBV)
   # most problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant
+  trywith 300 --full-saturate-quant --no-cbqi
   trywith 300 --full-saturate-quant --cbqi --decision=internal
   finishwith --finite-model-find
   ;;
 BV)
   trywith 300 --full-saturate-quant
+  trywith 300 --full-saturate-quant --no-cbqi
   finishwith --full-saturate-quant --cbqi --decision=internal
   ;;
 LIA|LRA)