From 52b210a1957eead903b82c835f8ffd4acde60840 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 12 Jun 2014 15:39:56 -0700
Subject: [PATCH] Modified run script for QF_AX

---
 contrib/run-script-smtcomp2014 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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
-- 
2.30.2