diff options
| author | Andres Nötzli <andres.noetzli@gmail.com> | 2017-06-16 20:07:17 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-06-16 20:07:17 -0700 |
| commit | 41f51ad4b0093611fa022629b15f1012a376f8e9 (patch) | |
| tree | 87811e42e4f296903aa0ded1b7ce7cc5ff419ef4 /contrib/run-script-smtcomp2017 | |
| parent | 0da095c3f5be79a85c085b4b46d7a0a0513ecdd6 (diff) | |
Change language in competition script to smt2.6 (#171)
* Change language in competition script to smt2.6
The benchmark scrambler for the application track cuts out
the :smt-lib-version command, so this commit sets it
manually to 2.6 (all benchmarks in SMT-COMP use the 2.6
standard) instead of 2.0. I have not seen any failures due
to that but might as well be prudent.
* Change language in competition script to smt2.6
The benchmark scrambler (at least for the application
track) cuts out the :smt-lib-version command, so this
commit sets it manually to 2.6 (all benchmarks in SMT-COMP
use the 2.6 standard) instead of 2.0. I have not seen any
failures due to that but might as well be prudent.
Diffstat (limited to 'contrib/run-script-smtcomp2017')
| -rw-r--r-- | contrib/run-script-smtcomp2017 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index 9e351d58e..b476203d5 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -11,7 +11,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_] # function returns normally. function trywith { limit=$1; shift; - result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)" + result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)" case "$result" in sat|unsat) echo "$result"; exit 0;; esac @@ -20,7 +20,7 @@ function trywith { # use: finishwith [params..] # to run cvc4 and let it output whatever it will to stdout. function finishwith { - $cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench + $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench } case "$logic" in @@ -118,7 +118,7 @@ QF_UFBV) finishwith --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_BV) - exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ + exec ./pcvc4 -L smt2.6 --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-abstraction' \ --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ |