[SMT-COMP] Remove --unconstrained-simp for incremental QF_LIA (#3333)

Fixes #3058. Commit a7c4cd3ecacb1e484a076edde0274c282bb43ffb changed
CVC4's behavior to emit an error when `--unconstrained-simp` is used
with `--incremental`. Before, we were silently disabling it. For some
reason, we had that option enabled for the incremental QF_LIA track of
SMT-COMP, so CVC4 failed on those benchmarks. This commit changes the
corresponding competition script to not use the option.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index 12c91a036cfb4070c1230932cd77da755cf80f66..84125f0065d46a3e616b4c70614eb56c821c0493 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -47,7 +47,7 @@ QF_BV)
   runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_LIA)
-  runcvc4 --tear-down-incremental=1 --unconstrained-simp
+  runcvc4 --tear-down-incremental=1
   ;;
 QF_UFBV)
   runcvc4 --incremental