summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2015-06-05 17:16:58 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2015-06-05 17:16:58 -0400
commit8f5698e5a2a9243743e5416a9b29a6b2086794a8 (patch)
tree4a77046ca78955747a732c012a034f15de7648c6 /contrib
parent217f7400cdccd1d11402d0739a3f688ef9d28e00 (diff)
pcvc4 with assertions
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/run-script-smtcomp2015-assertions2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions
index db35e3c93..3292e29fb 100755
--- a/contrib/run-script-smtcomp2015-assertions
+++ b/contrib/run-script-smtcomp2015-assertions
@@ -87,7 +87,7 @@ QF_ABV)
finishwith --ite-simp --simp-with-care --repeat-simp
;;
QF_BV)
- exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=256 \
+ exec ./pcvc4-assertions -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=256 \
--threads 2 \
--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 ' \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback