From 41f51ad4b0093611fa022629b15f1012a376f8e9 Mon Sep 17 00:00:00 2001 From: Andres Nötzli Date: Fri, 16 Jun 2017 20:07:17 -0700 Subject: 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. --- contrib/run-script-smtcomp2017 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'contrib/run-script-smtcomp2017') 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' \ -- cgit v1.2.3