Fix real as int for incremental (#3979)

Fixes #3956 and fixes #3969.

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index dba7ccbe3d3e823518c89b2bc2fad6ceb9c28b22..cc98726c6f9d8499c969a1b5e04f2ae343f020ea 100644 (file)
--- 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());
         }
       }
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aaf340ce79eacee612c8e842dff12c539b7e07e9..d449669a97276b2fa17957d70b904ab353866ce3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -689,6 +689,7 @@ set(regress_0_tests
   regress0/push-pop/issue2137.min.smt2
   regress0/push-pop/issue3915-real-as-int.smt2
   regress0/push-pop/quant-fun-proc-unfd.smt2
+  regress0/push-pop/real-as-int-incremental.smt2
   regress0/push-pop/simple_unsat_cores.smt2
   regress0/push-pop/test.00.cvc
   regress0/push-pop/test.01.cvc

diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
new file mode 100644 (file)
index 0000000..81af8c4
--- /dev/null
+++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --incremental --solve-real-as-int
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Real)
+(declare-fun y () Real)
+
+(assert (> x y))
+(assert (> x 500.5))
+
+(check-sat)
+
+(push 1)
+(declare-fun z () Real)
+(assert (> z x))
+(check-sat)
+(pop 1)
+
+(push 1)
+(declare-fun w () Real)
+(assert (> w x))
+(check-sat)
+(pop 1)