projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9642be1) | patch
Fix proof of nl lemma for a corner case (#7530)
authorGereon Kremer <nafur42@gmail.com>
Fri, 29 Oct 2021 22:37:39 +0000 (15:37 -0700)
committerGitHub <noreply@github.com>
Fri, 29 Oct 2021 22:37:39 +0000 (22:37 +0000)
commite86e6c20286af0eece976e7560b3dc400384f9c7
tree73bfed2f763edbbb2e94d3e798f2f9aa9fd45353tree
parent9642be1703c26e76ab5144a4993814fdb804a9b8commit | diff
Fix proof of nl lemma for a corner case (#7530)

This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.
src/theory/arith/nl/ext/monomial_bounds_check.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 [new file with mode: 0644] blob