Final update to SMT-COMP 2021 options (#6739)

This commit:

- Disables `--tear-down-incremental=X` for the competition since
  it currently does not work correctly on master and a fixed version did
  not show significant benefits.
- Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it
  is now a mode option.
- Removes the use of `--bv-assert-input` because the option currently
  has some issues in incremental mode (#6738)
- Removes the use of `--bitblast=eager` for the model validation track
  because it produces invalid models (#6741)

1 files changed, 5 insertions, 35 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index 21bb2f6e0..79df91d69 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 
 line=""
 while [[ -z "$line" ]]; do
@@ -26,50 +26,20 @@ function runcvc5 {
   # 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?)
-  $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
+  $cvc5 --incremental --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
 }
 
 case "$logic" in
 
-ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA)
-  runcvc5 --tear-down-incremental=1
-  ;;
 QF_AUFLIA)
-  runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
+  runcvc5 --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_BV)
-  runcvc5 --incremental --bitblast=eager --bv-assert-input
-  ;;
-QF_UFBV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-QF_UF)
-  runcvc5 --incremental
-  ;;
-QF_AUFBV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-QF_ABV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-ABVFP)
-  runcvc5 --incremental
-  ;;
-BVFP)
-  runcvc5 --incremental
-  ;;
-QF_ABVFP)
-  runcvc5 --incremental
-  ;;
-QF_BVFP)
-  runcvc5 --incremental
-  ;;
-QF_FP)
-  runcvc5 --incremental
+  runcvc5 --bitblast=eager
   ;;
 *)
   # just run the default
-  runcvc5 --incremental
+  runcvc5
   ;;
 
 esac