From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 15:00:07 +0000 (-0500)
Subject:  Fix real as int for incremental (#3979)
X-Git-Tag: cvc5-1.0.0~3533
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f57c7cb845c7d1f8730e1b3ecfa4d1c030b980ac;p=cvc5.git

 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 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());
         }
       }
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aaf340ce7..d449669a9 100644
--- 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
index 000000000..81af8c4e7
--- /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)