diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2015-06-15 10:20:55 +0100 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2015-06-15 10:20:55 +0100 |
| commit | 3034c5a560cd8dd880376fc5c0d6f7baccf759ed (patch) | |
| tree | 6edad5792b6ccfd65b8a61b6b3dcb241c4a91b30 | |
| parent | 6ce92a7e312cda1b1990082043589412aea3df5a (diff) | |
fixes to QF_BV and QF_UFBV run script
| -rwxr-xr-x | contrib/run-script-smtcomp2015 | 6 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-assertions | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index e32cb8049..97bcc9967 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -97,13 +97,13 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - finishwith --bitblast=eager --bv-sat-solver=cryptominisat --no-bv-native-xor + finishwith --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_BV) exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ --threads 2 \ - --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor' \ - --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ --no-wait-to-join \ "$bench" #trywith 10 --bv-eq-slicer=auto --decision=justification diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions index f0b6c1d18..9a79d793b 100755 --- a/contrib/run-script-smtcomp2015-assertions +++ b/contrib/run-script-smtcomp2015-assertions @@ -95,13 +95,13 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - finishwith --bitblast=eager --bv-sat-solver=cryptominisat --no-bv-native-xor + finishwith --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_BV) exec ./pcvc4-assertions -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ --threads 2 \ - --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor' \ - --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \ + --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor --no-bv-abstraction' \ + --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ --no-wait-to-join \ "$bench" #trywith 10 --bv-eq-slicer=auto --decision=justification |