projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7de44af) | patch
Fix dropped bounds on PI (#8164)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Feb 2022 17:15:00 +0000 (11:15 -0600)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 17:15:00 +0000 (17:15 +0000)
commit3428c0e156cdb3b079ae57bc8ba3805edb5d9c88
tree64a16ed148e6d21f360cb0ae5dbd55df72eb21cetree
parent7de44af3d352fe9f622945f8a61b2b1b4e6d8b49commit | diff
Fix dropped bounds on PI (#8164)

Fixes #8162.

In this example, we were failing to send the initial PI bound lemma, likely due to a conflict while this lemma was buffered.

This makes the PI refinement utility more robust by explicitly checking based on the model whether we need to refine PI.
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/issue8162-drop-pi-bound.smt2 [new file with mode: 0644] blob