projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a57702d) | patch
Prevent using the coverings solver with extended operators (#8523)
authorGereon Kremer <gkremer@cs.stanford.edu>
Fri, 1 Apr 2022 22:24:16 +0000 (00:24 +0200)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 22:24:16 +0000 (22:24 +0000)
commit0a58942a2eb87fd7e10d0cf2b54f2e7d0b9e5c26
treee28e4d7b158da91e4ae03fe61b1cb04b863844batree
parenta57702d1f24ffa9f84a6e50887138a00a48dac07commit | diff
Prevent using the coverings solver with extended operators (#8523)

The way we construct the model within the nonlinear extension makes using multiple subsolvers that contribute to the model potentially unsound. This PR prevent the coverings solver from being used if extended operators are present, unless --nl-cov-force is given.
Fixes #8515. Fixes #8516.
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8515-cov-iand.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/nl/issue8516-cov-sin.smt2 [new file with mode: 0644] blob