From 6ba68a1897838f3aefa6cbd254a1262326e446c7 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 29 Apr 2020 13:14:46 -0700
Subject: [PATCH] SMT-COMP 2020: Fix scripts to use --no-type-checking instead
 of --no-checking. (#4417)

---
 contrib/competitions/smt-comp/run-script-smtcomp-current      | 4 ++--
 .../smt-comp/run-script-smtcomp-current-incremental           | 2 +-
 .../smt-comp/run-script-smtcomp-current-model-validation      | 2 +-
 .../smt-comp/run-script-smtcomp-current-unsat-cores           | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index f2168398f..d4a257395 100755
--- 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 84125f006..d55c54b42 100755
--- 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 eec17294d..385a845e7 100755
--- 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 6cebad7fd..33f41263d 100755
--- 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
-- 
2.30.2