diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-15 01:29:53 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-15 01:29:53 -0400 |
commit | 6e7b111b9b38fb69ab10fbca11bd9144346fafd8 (patch) | |
tree | 1d480dedc1087aacc52fbd9aed914069d20fa668 /contrib | |
parent | 3452e2bd9344ec503329720f41e747510cebade5 (diff) |
better bv args for smtcomp
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/run-script-smtcomp2014 | 4 |
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 |