summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xcontrib/run-script-smtcomp2014-application2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index ae1d9e1ec..b04b33775 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -28,7 +28,7 @@ LIA|LRA|NIA|NRA)
runcvc4 --enable-cbqi --full-saturate-quant
;;
QF_BV)
- runcvc4 --bv-eq-slicer=auto --decision=justification
+ runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
;;
QF_AUFLIA|QF_AX)
runcvc4 --no-arrays-eager-index --arrays-eager-lemmas
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback