projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e252f83) | patch
Handle bitvector lemmas where a literal gets rewritten into false, and consequently...
authorGuy <katz911@gmail.com>
Fri, 1 Jul 2016 21:21:13 +0000 (14:21 -0700)
committerGuy <katz911@gmail.com>
Fri, 1 Jul 2016 21:21:13 +0000 (14:21 -0700)
commit1d4ad74ca90641bd9165f9a2c019c54cde6e80c1
treef6d1db1ca667a9c0e70b4a8f8b655e1a92a08627tree
parente252f83e7298fdbad1ac8882763e7571e7a83235commit | diff
Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict
src/proof/bitvector_proof.cpp diff | blob | history
src/proof/theory_proof.cpp diff | blob | history