projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5eb3476) | patch
Fix unsoundness in IAND solver (#8053)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Feb 2022 21:14:36 +0000 (15:14 -0600)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 21:14:36 +0000 (21:14 +0000)
commit328eeb2a34d333b05b60a7177a2eedffb4d17455
tree3ba9f2f77e3c4080022bfab192eea2f1ea6ec2b1tree
parent5eb347630fcccf038a8fae15946e35600bcc91aecommit | diff
Fix unsoundness in IAND solver (#8053)

Fixes #5461, fixes #8063. The initial lemma schema was assuming arguments were in bounds.

This also modifies the solver so that we throw logic exceptions when encountering iand or transcendentals.
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/issue5461-iand-init-refine.smt2 [new file with mode: 0644] blob