Fix type issue in substitutions from covering solver (#8921)

Fixes #8895. The benchmark in that issue now times out.

diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp
index dcc3cff945529895b78c31c8865e0c8e0dbee21a..23b773792aa96528137fe50361f47377f96ff625 100644 (file)
--- 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 4dcade0994787b33959b042258e54cc33df9797a..b0a498dc94b1b4afeec5edb41ae3822f12ace101 100644 (file)
--- 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 080a47d48e772872995b2e89d928cdb0c3b48fe1..e47abdac799630912859609bda1ea6f6be7a7f8d 100644 (file)
--- 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;