From f57c7cb845c7d1f8730e1b3ecfa4d1c030b980ac Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 10:00:07 -0500
Subject:  Fix real as int for incremental (#3979)

Fixes #3956 and fixes #3969.
---
 src/preprocessing/passes/real_to_int.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src')

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());
         }
       }
     }
-- 
cgit v1.2.3