projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 947b04a) | patch
Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)
authorMathias Preiner <mathias.preiner@gmail.com>
Sat, 6 Jan 2018 06:50:21 +0000 (22:50 -0800)
committerGitHub <noreply@github.com>
Sat, 6 Jan 2018 06:50:21 +0000 (22:50 -0800)
commitd26e19150d5d3a6cc8cee332a5f2067a7383a129
tree922eb51c3f5c27b39287d63af0463f5224189957tree
parent947b04aafc5d45fe901eccebc151f7a9c90de00ecommit | diff
Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)

This commit further fixes some other issues with bit-vectors of size 1.
src/theory/bv/theory_bv_utils.h diff | blob | history
src/theory/quantifiers/bv_inverter.cpp diff | blob | history