Fix linearization for terms where the solve variable does not occur. (#1506)

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]);