projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e1b546) | patch
[SMT-COMP] Remove --unconstrained-simp for incremental QF_LIA (#3333)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 2 Oct 2019 22:59:26 +0000 (15:59 -0700)
committerGitHub <noreply@github.com>
Wed, 2 Oct 2019 22:59:26 +0000 (15:59 -0700)
commit40ec51368b5ab23e74fb3537f307782f6c76ab22
tree9d7e765cea6a526c9cb7387c342dfbe21f8b265ftree
parent2e1b546811778f2c95f07b70f42e458b0552fab0commit | diff
[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.
contrib/competitions/smt-comp/run-script-smtcomp-current-incremental diff | blob | history