From ccc50ccd4b5021c5c83f350954ac1df27160184f Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 17 Dec 2021 12:48:38 -0800
Subject: [PATCH] Fix tracker in SubstitutionMap (#7829)

This PR fixes a subtle issue in #7787 where the rhs (instead of the lhs) of the applied substitution was inserted into the tracker.
Fixes cvc5/cvc5-projects#388
---
 src/theory/substitutions.cpp                |  2 +-
 test/unit/api/cpp/CMakeLists.txt            |  1 +
 test/unit/api/cpp/theory_arith_nl_black.cpp | 66 +++++++++++++++++++++
 3 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 test/unit/api/cpp/theory_arith_nl_black.cpp

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index e49563046..b56aa4f16 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -111,11 +111,11 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache, std::set<TNo
             internalSubstitute(rhs, cache, tracker);
             d_substitutions[result] = cache[rhs];
             cache[result] = cache[rhs];
-            result = cache[rhs];
             if (tracker != nullptr)
             {
               tracker->insert(result);
             }
+            result = cache[rhs];
           }
         }
       }
diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index e99732ca4..3e1330d6f 100644
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -22,3 +22,4 @@ cvc5_add_unit_test_white(solver_white api)
 cvc5_add_unit_test_black(sort_black api)
 cvc5_add_unit_test_black(term_black api)
 cvc5_add_unit_test_white(term_white api)
+cvc5_add_unit_test_black(theory_arith_nl_black api)
diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp
new file mode 100644
index 000000000..91f260a17
--- /dev/null
+++ b/test/unit/api/cpp/theory_arith_nl_black.cpp
@@ -0,0 +1,66 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Blackbox tests using the API targeting nonlinear arithmetic.
+ */
+
+#include "test_api.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestTheoryBlackArithNl : public TestApi
+{
+};
+
+TEST_F(TestTheoryBlackArithNl, cvc5Projects388)
+{
+  Solver slv;
+  slv.setLogic("QF_NRA");
+  Sort s = slv.getRealSort();
+  Term t1 = slv.mkConst(s, "a");
+  Term t2 = slv.mkConst(s, "b");
+  Term t3 = slv.mkConst(s, "c");
+  Term t4 = slv.mkTerm(Kind::DIVISION, {t1, t2});
+  Term t5 = slv.mkTerm(Kind::GT, {t4, t3});
+  Term t6 = slv.mkTerm(Kind::DIVISION, {t1, t3});
+  Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t6});
+  Term t8 = slv.mkTerm(Kind::AND, {t5, t7, t5});
+  Term t9 = slv.mkTerm(Kind::NOT, {t8});
+  slv.assertFormula(t9);
+  slv.checkSat();
+}
+
+TEST_F(TestTheoryBlackArithNl, cvc5Projects388Min)
+{
+  Solver slv;
+  slv.setOption("nl-cad", "true");
+  slv.setOption("nl-cad-var-elim", "true");
+  slv.setOption("nl-ext", "none");
+  slv.setLogic("QF_NIRA");
+  Sort s = slv.getRealSort();
+  Term t1 = slv.mkConst(s, "a");
+  Term t2 = slv.mkConst(s, "b");
+  Term t3 = slv.mkReal(0);
+  Term t7 = slv.mkTerm(Kind::IS_INTEGER, {t1});
+  Term t4 = slv.mkTerm(Kind::DIVISION, {t2, t1});
+  Term t5 = slv.mkTerm(Kind::DISTINCT, {t3, t4});
+  Term t8 = slv.mkTerm(Kind::OR, {t7, t5});
+  slv.assertFormula(t8);
+  slv.checkSat();
+}
+
+}  // namespace test
+}  // namespace cvc5
-- 
2.30.2