summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/run-script-smtcomp2014-application4
1 files changed, 3 insertions, 1 deletions
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
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback