Remove assertSkeleton for bag elements during model building (#7538)

This PR fixes a bug found by cvc5 fuzzy sygus.

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index f1014425592bfbba84544d49cde6bc8d829d23a5..4823c16e2584546ea6736a2c8fbfb7e1731f0bff 100644 (file)
--- 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<Node, Node> 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 6df6ebe762c9bba7abf71b0da3c33f42ffff587b..3f099cf671def05deee08d7a23a422674f48880b 100644 (file)
--- 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 (file)
index 0000000..dd6dd02
--- /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)