summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/run-script-smtcomp20144
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index cd81a3f52..55f274234 100755
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -72,8 +72,8 @@ QF_AUFBV)
QF_BV)
exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive \
--threads 2 \
- --thread0 '--unconstrained-simp --bv-eq-slicer=auto' \
- --thread1 '--bitblast=eager --unconstrained-simp' \
+ --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \
+ --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \
--no-wait-to-join \
"$bench"
#trywith 10 --bv-eq-slicer=auto --decision=justification
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback