From f80a5ed2b00cf0bc1d9ee8210dc64b3df7f8e6b4 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sun, 31 Oct 2021 08:50:38 -0500 Subject: [PATCH] Remove assertSkeleton for bag elements during model building (#7538) This PR fixes a bug found by cvc5 fuzzy sygus. --- src/theory/bags/theory_bags.cpp | 6 ------ test/regress/CMakeLists.txt | 1 + test/regress/regress1/bags/fuzzy3.smt2 | 13 +++++++++++++ 3 files changed, 14 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/bags/fuzzy3.smt2 diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index f10144255..4823c16e2 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -186,13 +186,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m, } Node rep = NormalForm::constructBagFromElements(tn, elementReps); rep = Rewriter::rewrite(rep); - Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl; - for (std::pair pair : elementReps) - { - m->assertSkeleton(pair.first); - m->assertSkeleton(pair.second); - } m->assertEquality(rep, n, true); m->assertSkeleton(rep); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6df6ebe76..3f099cf67 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1590,6 +1590,7 @@ set(regress_1_tests regress1/bags/emptybag1.smt2 regress1/bags/fuzzy1.smt2 regress1/bags/fuzzy2.smt2 + regress1/bags/fuzzy3.smt2 regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 new file mode 100644 index 000000000..dd6dd02dc --- /dev/null +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun B () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (not + (= + (= A (difference_remove (bag d c) A)) + (= A (bag (tuple c c) c))))) +(check-sat) -- 2.30.2