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 | |
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')
-rw-r--r-- | contrib/run-script-smtcomp2017 | 6 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2017-application | 2 |
2 files changed, 4 insertions, 4 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' \ diff --git a/contrib/run-script-smtcomp2017-application b/contrib/run-script-smtcomp2017-application index ddcc1f0c6..8a8ea7786 100755 --- a/contrib/run-script-smtcomp2017-application +++ b/contrib/run-script-smtcomp2017-application @@ -26,7 +26,7 @@ function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive "$@" <&0- + $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0- } case "$logic" in |