projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 706dbda) | patch
Do not use relevance during non-linear check model (#4938)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 24 Aug 2020 19:29:40 +0000 (14:29 -0500)
committerGitHub <noreply@github.com>
Mon, 24 Aug 2020 19:29:40 +0000 (14:29 -0500)
commitdf2150c721b811a588e5f731b6bc11b236ee3a7e
tree580d1d55b4655c1f213ac25944b2cd4b93747aeftree
parent706dbdac95131bf45efbfcb9a8ca4df9dfb85478commit | diff
Do not use relevance during non-linear check model (#4938)

This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history