From e91881e9afc5ab4ca2ce7c1d0a1357c8a006462a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 May 2022 13:33:30 -0500
Subject: [PATCH] Fix mixed arithmetic issue in relevant domain (#8826)

Fixes #8821.
---
 src/theory/quantifiers/relevant_domain.cpp    | 24 ++++++++++++-------
 test/regress/cli/CMakeLists.txt               |  1 +
 .../issue8821-enum-interleave-types.smt2      |  5 ++++
 3 files changed, 22 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/cli/regress0/quantifiers/issue8821-enum-interleave-types.smt2

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index fc1e6b549..0f103ec43 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -149,7 +149,8 @@ void RelevantDomain::compute(){
         }
       }
     }
-    //print debug
+    // print debug and verify types are correct
+    NodeManager* nm = NodeManager::currentNM();
     for (std::pair<const Node, std::map<size_t, RDomain*> >& d : d_rel_doms)
     {
       Trace("rel-dom") << "Relevant domain for " << d.first << " : "
@@ -166,17 +167,24 @@ void RelevantDomain::compute(){
           Trace("rel-dom") << "Dom( " << d.first << ", " << dd.first << " ) ";
         }
         Trace("rel-dom") << std::endl;
-        if (Configuration::isAssertionBuild())
+        if (d.first.getKind() == FORALL)
         {
-          if (d.first.getKind() == FORALL)
+          TypeNode expectedType = d.first[0][dd.first].getType();
+          for (Node& t : r->d_terms)
           {
-            TypeNode expectedType = d.first[0][dd.first].getType();
-            for (const Node& t : r->d_terms)
+            TypeNode tt = t.getType();
+            if (tt != expectedType)
             {
-              if (t.getType() != expectedType)
+              // Computation may merge Int with Real due to inequalities. We
+              // correct this here.
+              if (tt.isInteger() && expectedType.isReal())
+              {
+                t = nm->mkNode(TO_REAL, t);
+              }
+              else
               {
-                Unhandled() << "Relevant domain: bad type " << t.getType()
-                            << ", expected " << expectedType;
+                Assert(false) << "Relevant domain: bad type " << t.getType()
+                              << ", expected " << expectedType;
               }
             }
           }
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 67deaccaf..614d5fc1b 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1087,6 +1087,7 @@ set(regress_0_tests
   regress0/quantifiers/issue8227-subs-shadow.smt2
   regress0/quantifiers/issue8466-syqi-bool.smt2
   regress0/quantifiers/issue8609-subtype-assert.smt2
+  regress0/quantifiers/issue8821-enum-interleave-types.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/issue8821-enum-interleave-types.smt2 b/test/regress/cli/regress0/quantifiers/issue8821-enum-interleave-types.smt2
new file mode 100644
index 000000000..e874339a3
--- /dev/null
+++ b/test/regress/cli/regress0/quantifiers/issue8821-enum-interleave-types.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --enum-inst-interleave
+; EXPECT: unsat
+(set-logic ALL)
+(assert (forall ((a Real)) (or (> 0 a) (> a 0.0))))
+(check-sat)
-- 
2.30.2