From: Andres Noetzli Date: Wed, 2 Oct 2019 22:59:26 +0000 (-0700) Subject: [SMT-COMP] Remove --unconstrained-simp for incremental QF_LIA (#3333) X-Git-Tag: cvc5-1.0.0~3921 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40ec51368b5ab23e74fb3537f307782f6c76ab22;p=cvc5.git [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 12c91a036..84125f006 100755 --- 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