diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-09-01 08:47:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-01 13:47:26 +0000 |
| commit | 7f4ceaabbfa36408bf5a0c63a9051417be9d4819 (patch) | |
| tree | cb947309876b6b8667fb9bb9f7c96cb636848b7d | |
| parent | 12fd4e1a87a33dc541a71747a9a3250fe3854aa9 (diff) | |
Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)
Fixed TestTheoryWhiteBagsRewriter.map failure
| -rw-r--r-- | test/unit/theory/theory_bags_rewriter_white.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
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); |