From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 1 Sep 2021 13:47:26 +0000 (-0500)
Subject: Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)
X-Git-Tag: cvc5-1.0.0~1306
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f4ceaabbfa36408bf5a0c63a9051417be9d4819;p=cvc5.git

Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)

Fixed TestTheoryWhiteBagsRewriter.map failure
---

diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index e63fb3b20..a05d76437 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -697,8 +697,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set)
 
 TEST_F(TestTheoryWhiteBagsRewriter, map)
 {
-  Node emptybagString =
-      d_nodeManager->mkConst(EmptyBag(d_nodeManager->stringType()));
+  TypeNode bagStringType =
+      d_nodeManager->mkBagType(d_nodeManager->stringType());
+  Node emptybagString = d_nodeManager->mkConst(EmptyBag(bagStringType));
 
   Node one = d_nodeManager->mkConst(Rational(1));
   Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
@@ -710,8 +711,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   // (bag.map (lambda ((x U))  t) emptybag) = emptybag
   Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString);
   RewriteResponse response1 = d_rewriter->postRewrite(n1);
-  TypeNode type = d_nodeManager->mkBagType(d_nodeManager->integerType());
-  Node emptybagInteger = d_nodeManager->mkConst(EmptyBag(type));
+  TypeNode bagIntType = d_nodeManager->mkBagType(d_nodeManager->integerType());
+  Node emptybagInteger = d_nodeManager->mkConst(EmptyBag(bagIntType));
   ASSERT_TRUE(response1.d_node == emptybagInteger
               && response1.d_status == REWRITE_AGAIN_FULL);