4 files changed, 38 insertions, 50 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be7c5c665..b4d3b013d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -749,15 +749,6 @@ Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
 
 Sort::~Sort() {}
 
-Sort& Sort::operator=(const Sort& s)
-{
-  if (this != &s)
-  {
-    *d_type = *s.d_type;
-  }
-  return *this;
-}
-
 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
@@ -1008,15 +999,6 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 Term::~Term() {}
 
-Term& Term::operator=(const Term& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
@@ -1180,15 +1162,6 @@ OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 OpTerm::~OpTerm() {}
 
-OpTerm& OpTerm::operator=(const OpTerm& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
 
 bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index fc07a1cd7..aebeffb0d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -197,13 +197,6 @@ class CVC4_PUBLIC Sort
   ~Sort();
 
   /**
-   * Assignment operator.
-   * @param s the sort to assign to this sort
-   * @return this sort after assignment
-   */
-  Sort& operator=(const Sort& s);
-
-  /**
    * Comparison for structural equality.
    * @param s the sort to compare to
    * @return true if the sorts are equal
@@ -554,14 +547,6 @@ class CVC4_PUBLIC Term
   ~Term();
 
   /**
-   * Assignment operator, makes a copy of the given term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this term after assignment
-   */
-  Term& operator=(const Term& t);
-
-  /**
    * Syntactic equality operator.
    * Return true if both terms are syntactically identical.
    * Both terms must belong to the same solver object.
@@ -844,14 +829,6 @@ class CVC4_PUBLIC OpTerm
   ~OpTerm();
 
   /**
-   * Assignment operator, makes a copy of the given operator term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this operator term after assignment
-   */
-  OpTerm& operator=(const OpTerm& t);
-
-  /**
    * Syntactic equality operator.
    * Return true if both operator terms are syntactically identical.
    * Both operator terms must belong to the same solver object.
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 90d34f7c6..025575e41 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -2,3 +2,4 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(api_guards_black api)
+cvc4_add_unit_test_black(term_black api)
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
new file mode 100644
index 000000000..c2ca1cb08
--- /dev/null
+++ b/test/unit/api/term_black.h
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file term_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Black box testing of the Term class
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class TermBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testTermAssignment()
+  {
+    Term t1 = d_solver.mkReal(1);
+    Term t2 = t1;
+    t2 = d_solver.mkReal(2);
+    TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+  }
+
+ private:
+  Solver d_solver;
+};