From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 13 Jun 2014 05:26:03 +0000 (-0400)
Subject: Adjust incremental run script for QF_AX too.
X-Git-Tag: cvc5-1.0.0~6825
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1fb2fdaad36fa6c2a7d7b9ead2914b8779280781;p=cvc5.git

Adjust incremental run script for QF_AX too.
---

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index 3703dcd2f..c754818b7 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -30,10 +30,12 @@ LIA|LRA|NIA|NRA)
 QF_BV)
   runcvc4 --bv-eq-slicer=auto --decision=justification
   ;;
+QF_AX)
+  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
 *)
   # just run the default
   runcvc4
   ;;
 
 esac
-