From f5bd085bb7c5c725bc11f804359f74cdb15e761b Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Thu, 10 Mar 2022 12:49:31 -0600
Subject: [PATCH] Fix cvc5-projects issue 475 (#8278)

Fixes cvc5/cvc5-projects#475.
---
 src/theory/bags/inference_generator.cpp | 2 +-
 test/regress/CMakeLists.txt             | 1 +
 test/regress/regress1/bags/murxla4.smt2 | 5 +++++
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/bags/murxla4.smt2

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index b87296f32..2aab8473d 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -175,7 +175,7 @@ Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
 InferInfo InferenceGenerator::empty(Node n, Node e)
 {
   Assert(n.getKind() == BAG_EMPTY);
-  Assert(e.getType() == n.getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
 
   InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
   Node skolem = getSkolem(n, inferInfo);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fdbe1ed55..30311558d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1752,6 +1752,7 @@ set(regress_1_tests
   regress1/bags/murxla1.smt2
   regress1/bags/murxla2.smt2
   regress1/bags/murxla3.smt2
+  regress1/bags/murxla4.smt2
   regress1/bags/product1.smt2
   regress1/bags/product2.smt2
   regress1/bags/product3.smt2
diff --git a/test/regress/regress1/bags/murxla4.smt2 b/test/regress/regress1/bags/murxla4.smt2
new file mode 100644
index 000000000..9f2d1b259
--- /dev/null
+++ b/test/regress/regress1/bags/murxla4.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x Int)
+(assert ((_ divisible 2) (bag.count 0.0 (bag 0.0 x))))
+(check-sat)
-- 
2.30.2