diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-01-09 18:12:32 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-09 18:12:32 -0800 |
commit | ff9d2c84dae5eb21a7ef77f5931673fb23129730 (patch) | |
tree | 567463672f28f8b8f626c0bfc3e6b20f3798a6f4 /test/unit | |
parent | fa378358488a5bc2525dde852fcc9cbdeee9283e (diff) |
Fix linearization for terms where the solve variable does not occur. (#1506)
Diffstat (limited to 'test/unit')
-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]); |