diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_instantiator_white.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 1f3932be0..1e6578b27 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -162,6 +162,10 @@ void BvInstantiatorWhite::testNormalizePvMult() Node norm_xx = normalizePvMult(x, {x, neg_x}, contains_x); TS_ASSERT(norm_xx.isNull()); + /* nothing to normalize -> create a * a */ + Node norm_aa = normalizePvMult(x, {a, a}, contains_x); + TS_ASSERT(norm_aa == Rewriter::rewrite(mkMult(a, a))); + /* normalize x * a -> x * a */ Node norm_xa = normalizePvMult(x, {x, a}, contains_x); TS_ASSERT(contains_x[norm_xa]); @@ -258,6 +262,10 @@ void BvInstantiatorWhite::testNormalizePvPlus() Node norm_abx = normalizePvPlus(x, {a, mult_bx}, contains_x); TS_ASSERT(norm_abx.isNull()); + /* nothing to normalize -> create a + a */ + Node norm_aa = normalizePvPlus(x, {a, a}, contains_x); + TS_ASSERT(norm_aa == Rewriter::rewrite(mkPlus(a, a))); + /* x + a -> x + a */ Node norm_xa = normalizePvPlus(x, {x, a}, contains_x); TS_ASSERT(contains_x[norm_xa]); |