From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Apr 2022 13:16:49 +0000 (-0500)
Subject: Fix spurious assertion involving subtypes (#8611)
X-Git-Tag: cvc5-1.0.1~264
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ab7a86c46ebeab243a768a6240c2ecfb0b7464d;p=cvc5.git

Fix spurious assertion involving subtypes (#8611)

Fixes #8609.
---

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index f09faf22f..dbb6c6acc 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1234,7 +1234,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             Node v = msum_term[it->first];
             if (!v.isNull())
             {
-              Assert(v.getType() == type);
+              Assert(v.getType().isComparableTo(type));
               c = nm->mkNode(MULT, c, v);
             }
             children.push_back( c );
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 99ca3b969..dbdd97c83 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1061,6 +1061,7 @@ set(regress_0_tests
   regress0/quantifiers/issue8159-3-qext-nterm.smt2
   regress0/quantifiers/issue8227-subs-shadow.smt2
   regress0/quantifiers/issue8466-syqi-bool.smt2
+  regress0/quantifiers/issue8609-subtype-assert.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
diff --git a/test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2 b/test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2
new file mode 100644
index 000000000..a85afb034
--- /dev/null
+++ b/test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(set-info :status unsat)
+(assert (forall ((r Int) (r9 Int)) (= 1.0 (/ (to_real r) (+ 0.5 (to_real r9))))))
+(check-sat)