projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cef98b9) | patch
Add unit tests for BitVector, minor BV rewrite fix (#1622)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 24 Feb 2018 02:02:53 +0000 (18:02 -0800)
committerGitHub <noreply@github.com>
Sat, 24 Feb 2018 02:02:53 +0000 (18:02 -0800)
commitcb8e3b305ecf83cde0380f9198fa6d3f795362cd
treecbae726a0df059c89bdbfaaf36fcb3f356e7d298tree
parentcef98b9c073c6c1a1535f4f45589a86cfaab1c33commit | diff
Add unit tests for BitVector, minor BV rewrite fix (#1622)

This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
src/util/bitvector.cpp diff | blob | history
test/unit/util/bitvector_black.h diff | blob | history