diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-02-23 18:02:53 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-23 18:02:53 -0800 |
commit | cb8e3b305ecf83cde0380f9198fa6d3f795362cd (patch) | |
tree | cbae726a0df059c89bdbfaaf36fcb3f356e7d298 /src/theory/bv | |
parent | cef98b9c073c6c1a1535f4f45589a86cfaab1c33 (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.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d91067d1e..a4be19253 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1303,10 +1303,13 @@ inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) { t = node[1][0]; c = node[0]; } - BitVector bv_c = c.getConst<BitVector>(); - BitVector bv_max = - BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1); + if (utils::getSize(t) == utils::getSize(c)) + { + return false; + } + + BitVector bv_c = c.getConst<BitVector>(); BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t)); BitVector zero = BitVector(c_hi.getSize(), Integer(0)); |