From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Feb 2020 00:20:25 +0000 (-0600)
Subject: Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)
X-Git-Tag: cvc5-1.0.0~3655
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0858188716609ae8a45e542bc4e054e675f2676d;p=cvc5.git

Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)

* Fix non-linear equality solving that involves mixed real/integer.

* Format

* Fix

* Revert

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
---

diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 54ae4c52a..8a4145552 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -534,8 +534,11 @@ bool NlModel::solveEqualitySimple(Node eq,
         if (ArithMSum::isolate(uv, msum, veqc, slv, EQUAL) != 0)
         {
           Assert(!slv.isNull());
-          // currently do not support substitution-with-coefficients
-          if (veqc.isNull() && !expr::hasSubterm(slv, uv))
+          // Currently do not support substitution-with-coefficients.
+          // We also ensure types are correct here, which avoids substituting
+          // a term of non-integer type for a variable of integer type.
+          if (veqc.isNull() && !expr::hasSubterm(slv, uv)
+              && slv.getType().isSubtypeOf(uv.getType()))
           {
             Trace("nl-ext-cm")
                 << "check-model-subs : " << uv << " -> " << slv << std::endl;