From c501613c172412b579884b37ed3133a8bbb06f09 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 29 Jun 2022 23:54:56 -0500
Subject: [PATCH] Fix type issue in substitutions from covering solver (#8921)

Fixes #8895. The benchmark in that issue now times out.
---
 src/theory/arith/nl/coverings_solver.cpp | 14 ++++++++++++--
 src/theory/arith/nl/nl_model.cpp         |  2 ++
 src/theory/arith/theory_arith.cpp        |  6 ++++--
 3 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp
index dcc3cff94..23b773792 100644
--- a/src/theory/arith/nl/coverings_solver.cpp
+++ b/src/theory/arith/nl/coverings_solver.cpp
@@ -249,9 +249,19 @@ void CoveringsSolver::addToModel(TNode var, TNode value) const
   // reductions inference of the sine solver) may have introduced substitutions
   // internally during check.
   Node svalue = d_model.getSubstitutedForm(value);
-  if (var.getType().isInteger() && svalue.getKind() == Kind::TO_REAL)
+  // ensure the value has integer type if var has integer type
+  if (var.getType().isInteger())
   {
-    svalue = svalue[0];
+    if (svalue.getKind() == Kind::TO_REAL)
+    {
+      svalue = svalue[0];
+    }
+    else if (svalue.getKind() == Kind::CONST_RATIONAL)
+    {
+      Assert(svalue.getConst<Rational>().isIntegral());
+      svalue =
+          NodeManager::currentNM()->mkConstInt(svalue.getConst<Rational>());
+    }
   }
   Trace("nl-cov") << "-> " << var << " = " << svalue << std::endl;
   d_model.addSubstitution(var, svalue);
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 4dcade099..b0a498dc9 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -274,6 +274,8 @@ bool NlModel::addSubstitution(TNode v, TNode s)
                         << std::endl;
   Assert(getSubstitutedForm(s) == s)
       << "Added a substitution whose range is not in substituted form " << s;
+  // cannot substitute real for integer
+  Assert(v.getType().isReal() || s.getType().isInteger());
   // should not substitute the same variable twice
   // should not set exact bound more than once
   if (d_substitutions.contains(v))
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 080a47d48..e47abdac7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -337,7 +337,8 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
       continue;
     }
     // maps to constant of same type
-    Assert(p.first.getType() == p.second.getType());
+    Assert(p.first.getType() == p.second.getType())
+        << "Bad type : " << p.first << " -> " << p.second;
     if (m->assertEquality(p.first, p.second, true))
     {
       continue;
@@ -438,7 +439,8 @@ bool TheoryArith::sanityCheckIntegerModel()
   {
     for (CVC5_UNUSED const auto& p : d_arithModelCache)
     {
-      Assert(p.first.getType() == p.second.getType());
+      Assert(p.first.getType() == p.second.getType())
+          << "Bad type: " << p.first << " -> " << p.second;
     }
   }
   bool addedLemma = false;
-- 
2.30.2