Fix issue 5513 (#5757)

Fix issue5513 by throwing an exception for unsupported bag operators

2 files changed, 20 insertions, 3 deletions

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index b3251e464..21a9d0e53 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -182,7 +182,24 @@ TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
 
 Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
 
-void TheoryBags::preRegisterTerm(TNode node) {}
+void TheoryBags::preRegisterTerm(TNode n)
+{
+  Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
+  switch (n.getKind())
+  {
+    case BAG_CARD:
+    case BAG_FROM_SET:
+    case BAG_TO_SET:
+    case BAG_IS_SINGLETON:
+    case DUPLICATE_REMOVAL:
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << n.getKind() << " is not supported yet";
+      throw LogicException(ss.str());
+    }
+    default: break;
+  }
+}
 
 TrustNode TheoryBags::expandDefinition(Node n)
 {
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 09784add9..aeae3810e 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -22,8 +22,8 @@
 #include "theory/bags/bag_solver.h"
 #include "theory/bags/bags_rewriter.h"
 #include "theory/bags/bags_statistics.h"
-#include "theory/bags/inference_manager.h"
 #include "theory/bags/inference_generator.h"
+#include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
@@ -70,7 +70,7 @@ class TheoryBags : public Theory
   TrustNode explain(TNode) override;
   Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_BAGS"; }
-  void preRegisterTerm(TNode node) override;
+  void preRegisterTerm(TNode n) override;
   TrustNode expandDefinition(Node n) override;
   void presolve() override;