From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 12 Jun 2014 22:39:56 +0000 (-0700)
Subject: Modified run script for QF_AX
X-Git-Tag: cvc5-1.0.0~6826
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52b210a1957eead903b82c835f8ffd4acde60840;p=cvc5.git

Modified run script for QF_AX
---

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index 454763cac..a12cd4471 100755
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -76,8 +76,7 @@ QF_BV)
   finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
   ;;
 QF_AX)
-  trywith 2
-  finishwith --no-arrays-model-based
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 *)
   # just run the default