SMT-COMP 2020: Fix scripts to use --no-type-checking instead of --no-checking. (...

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index f2168398fcab6a812ddf3e98feeab9cf80d54178..d4a25739588d6d4b99efa814c0dc972e9f3dd156 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -11,7 +11,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # returns normally and prints the output of the solver to stderr.
 function trywith {
   limit=$1; shift;
-  result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)"
+  result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
     *)         echo "$result" >&2;;
@@ -21,7 +21,7 @@ function trywith {
 # use: finishwith [params..]
 # to run cvc4 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
 }
 
 # the following is designed for a run time of 20 min.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index 84125f0065d46a3e616b4c70614eb56c821c0493..d55c54b428246215ef6649d054a395ccae41b1f0 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -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.6 --print-success --no-checking --no-interactive "$@" <&0-
+  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
 }
 
 case "$logic" in

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
index eec17294d0b3c5b25c7cff64869e989e2dff0c5f..385a845e7071341714357f86c3a5414ee05e5530 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
@@ -8,7 +8,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # use: finishwith [params..]
 # to run cvc4 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 6cebad7fd0dbe6c09b8a6425fe5bdd06be6d0df0..33f41263da5e9e549985b4222a35462bc3b85aa0 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -8,7 +8,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # use: finishwith [params..]
 # to run cvc4 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in