4 files changed, 58 insertions, 2 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ecec6f8c3..165854476 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1060,7 +1060,15 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
                   .toType());
 }
 
-std::string Sort::toString() const { return d_type->toString(); }
+std::string Sort::toString() const
+{
+  if (d_solver != nullptr)
+  {
+    NodeManagerScope scope(d_solver->getNodeManager());
+    return d_type->toString();
+  }
+  return d_type->toString();
+}
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
@@ -1481,6 +1489,11 @@ std::string Op::toString() const
   {
     CVC4_API_CHECK(!d_node->isNull())
         << "Expecting a non-null internal expression";
+    if (d_solver != nullptr)
+    {
+      NodeManagerScope scope(d_solver->getNodeManager());
+      return d_node->toString();
+    }
     return d_node->toString();
   }
 }
@@ -1858,7 +1871,15 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
   }
 }
 
-std::string Term::toString() const { return d_node->toString(); }
+std::string Term::toString() const
+{
+  if (d_solver != nullptr)
+  {
+    NodeManagerScope scope(d_solver->getNodeManager());
+    return d_node->toString();
+  }
+  return d_node->toString();
+}
 
 Term::const_iterator::const_iterator()
     : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index 65f6e9e57..da0bc8427 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -31,6 +31,8 @@ class OpBlack : public CxxTest::TestSuite
   void testGetIndicesUint();
   void testGetIndicesPairUint();
 
+  void testOpScopingToString();
+
  private:
   Solver d_solver;
 };
@@ -185,3 +187,11 @@ void OpBlack::testGetIndicesPairUint()
   TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
                    CVC4ApiException&);
 }
+
+void OpBlack::testOpScopingToString()
+{
+  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  std::string op_repr = bitvector_repeat_ot.toString();
+  Solver solver2;
+  TS_ASSERT_EQUALS(bitvector_repeat_ot.toString(), op_repr);
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index e9f0e04ea..02e5d814d 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -54,6 +54,8 @@ class SortBlack : public CxxTest::TestSuite
   void testSortCompare();
   void testSortSubtyping();
 
+  void testSortScopedToString();
+
  private:
   Solver d_solver;
 };
@@ -385,3 +387,15 @@ void SortBlack::testSortSubtyping()
   TS_ASSERT(!setSortR.isComparableTo(setSortI));
   TS_ASSERT(!setSortR.isSubsortOf(setSortI));
 }
+
+void SortBlack::testSortScopedToString()
+{
+  std::string name = "uninterp-sort";
+  Sort bvsort8 = d_solver.mkBitVectorSort(8);
+  Sort uninterp_sort = d_solver.mkUninterpretedSort(name);
+  TS_ASSERT_EQUALS(bvsort8.toString(), "(_ BitVec 8)");
+  TS_ASSERT_EQUALS(uninterp_sort.toString(), name);
+  Solver solver2;
+  TS_ASSERT_EQUALS(bvsort8.toString(), "(_ BitVec 8)");
+  TS_ASSERT_EQUALS(uninterp_sort.toString(), name);
+}
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index cb8ad944a..786b60bb3 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -46,6 +46,8 @@ class TermBlack : public CxxTest::TestSuite
   void testConstArray();
   void testConstSequenceElements();
 
+  void testTermScopedToString();
+
  private:
   Solver d_solver;
 };
@@ -796,3 +798,12 @@ void TermBlack::testConstSequenceElements()
   Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
   TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&);
 }
+
+void TermBlack::testTermScopedToString()
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+  TS_ASSERT_EQUALS(x.toString(), "x");
+  Solver solver2;
+  TS_ASSERT_EQUALS(x.toString(), "x");
+}