From 40ec51368b5ab23e74fb3537f307782f6c76ab22 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 2 Oct 2019 15:59:26 -0700 Subject: [PATCH] [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. --- .../smt-comp/run-script-smtcomp-current-incremental | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.30.2