From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 5 Jun 2015 21:16:58 +0000 (-0400)
Subject: pcvc4 with assertions
X-Git-Tag: cvc5-1.0.0~6303
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f5698e5a2a9243743e5416a9b29a6b2086794a8;p=cvc5.git

pcvc4 with assertions
---

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 ' \