projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1210cf5) | patch
Enable nl-cov-var-elim by default, but disable with proofs (#8310)
authorGereon Kremer <gkremer@cs.stanford.edu>
Tue, 15 Mar 2022 18:25:21 +0000 (19:25 +0100)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 18:25:21 +0000 (18:25 +0000)
commitaedccbd629c5af0cbc960a170fad47f10f332da9
tree0898a93983523a87dd39f0078d63b4d7f2e4c497tree
parent1210cf5b69466ee910da1208420ef718cfa96be6commit | diff
Enable nl-cov-var-elim by default, but disable with proofs (#8310)

This changes our policy for --nl-cov-var-elim. It is now enabled by default (it is only used when the coverings solver is used, though), but then disabled when proofs are enabled. Before, it was forced to be enabled when coverings were enabled in set_defaults.

Fixes cvc5/cvc5-projects#489
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history