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.

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index 9e351d58ed7d2e5ffc5af38ce2960d9ae712d6b4..b476203d5359af9e937734170f554d0199133a08 100644 (file)
--- 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 ddcc1f0c68fea10d4ca526eb3a62fc968d2a2060..8a8ea77866e5c7c83e82380130735a59b2b02283 100755 (executable)
--- 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