Fix real as int for incremental (#3979)

Fixes #3956 and fixes #3969.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index dba7ccbe3..cc98726c6 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -171,8 +171,11 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
                              nm->integerType(),
                              "Variable introduced in realToIntInternal pass");
           var_eq.push_back(n.eqNode(ret));
-          TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
-          m->addSubstitution(n, ret);
+          // ensure that the original variable is defined to be the returned
+          // one, which is important for models and for incremental solving.
+          std::vector<Expr> args;
+          smt::currentSmtEngine()->defineFunction(
+              n.toExpr(), args, ret.toExpr());
         }
       }
     }