projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f57c7cb) | patch
Do not set values for non-linear mult terms in collectModelInfo (#3983)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 10 Mar 2020 15:56:58 +0000 (10:56 -0500)
committerGitHub <noreply@github.com>
Tue, 10 Mar 2020 15:56:58 +0000 (08:56 -0700)
commit54eb1c069f0a86b157945d95eb0ae0999d8470fd
treef062eb87026b52315d8b7867a5d7a503e1b05b0dtree
parentf57c7cb845c7d1f8730e1b3ecfa4d1c030b980accommit | diff
Do not set values for non-linear mult terms in collectModelInfo (#3983)

Fixes #3803.

When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.
src/theory/arith/nl_model.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/issue3803-nl-check-model.smt2 [new file with mode: 0644] blob