2 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 46be960c7..1c8b9611f 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1485,16 +1485,19 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
     // no non-linear constraints, we are done
     return;
   }
+  Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
   d_model.reset(d_containing.getValuation().getModel(), arithModel);
   // run a last call effort check
   d_cmiLemmas.clear();
   d_cmiLemmasPp.clear();
   if (!d_builtModel.get())
   {
+    Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
     modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp);
   }
   if (d_builtModel.get())
   {
+    Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
     d_approximations.clear();
     // modify the model values
     d_model.getModelValueRepair(arithModel, d_approximations);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b8bdd04e1..2b8ce922d 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4376,6 +4376,16 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
     {
       if (!m->assertEquality(p.first, p.second, true))
       {
+        // If we failed to assert an equality, it is likely due to theory
+        // combination, namely the repaired model for non-linear changed
+        // an equality status that was agreed upon by both (linear) arithmetic
+        // and another theory. In this case, we must add a lemma, or otherwise
+        // we would terminate with an invalid model. Thus, we add a splitting
+        // lemma of the form ( x = v V x != v ) where v is the model value
+        // assigned by the non-linear solver to x.
+        Node eq = p.first.eqNode(p.second);
+        Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
+        d_containing.d_out->lemma(lem);
         return false;
       }
     }