Fix mixed arithmetic issue in relevant domain (#8826)

Fixes #8821.

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index fc1e6b54993856a632422cf90d15177c68526867..0f103ec43dc5992b45bb3ae899685b2bab8371bd 100644 (file)
--- 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 67deaccaf1379ee08dc267e71ed0cb6f5b13c8f9..614d5fc1be3fc15bbdd3661ec5dba2702c80184f 100644 (file)
--- 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 (file)
index 0000000..e874339
--- /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)