projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4d9c7c7) | patch
Fix check for whether PI is reduced (#8485)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2022 18:05:53 +0000 (13:05 -0500)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 18:05:53 +0000 (18:05 +0000)
commit3c53479aab2d7bb086a9d25acd0417c60b98affc
tree459a64ba28894368dfa4e9e08de701982b641416tree
parent4d9c7c7557b38a5999284a14857d26be19352f57commit | diff
Fix check for whether PI is reduced (#8485)

Fixes cvc5/cvc5-projects#505.

Also fixes a counter-intuitive behavior where 0 was not considered reduced and does minor cleanup.
src/theory/arith/nl/ext_theory_callback.cpp diff | blob | history
src/theory/arith/nl/ext_theory_callback.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/nta/pi-simplest.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2 [new file with mode: 0644] blob