From 0858188716609ae8a45e542bc4e054e675f2676d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Feb 2020 18:20:25 -0600 Subject: [PATCH] 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> --- src/theory/arith/nl_model.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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; -- 2.30.2