17 files changed, 640 insertions, 492 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5aea954e3..5304fcab5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -157,6 +157,8 @@ set(regress_0_tests
   regress0/buggy-ite.smt2
   regress0/bv/ackermann1.smt2
   regress0/bv/ackermann2.smt2
+  regress0/bv/ackermann3.smt2
+  regress0/bv/ackermann4.smt2
   regress0/bv/bool-to-bv.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
@@ -171,7 +173,8 @@ set(regress_0_tests
   regress0/bv/bv-options2.smt2
   regress0/bv/bv-options3.smt2
   regress0/bv/bv-options4.smt2
-  regress0/bv/bv-to-bool.smt
+  regress0/bv/bv-to-bool1.smt
+  regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvmul-pow2-only.smt2
@@ -836,6 +839,7 @@ set(regress_0_tests
   regress0/strings/substr-rewrites.smt2
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
+  regress0/strings/unsound-repl-rewrite.smt2
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
   regress0/sygus/c100.sy
diff --git a/test/regress/README.md b/test/regress/README.md
index d43ebf337..28ccfb96b 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -3,20 +3,10 @@
 ## Regression Levels and Running Regression Tests
 
 CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher
-regression levels are reserved for longer running regressions. To run
-regressions up to a certain level use `make regressX` where `X` designates the
-level. `make regress` by default runs levels 0 and 1. On Travis, we only run
-regression level 0 to keep the time short. During our nightly builds, we run
-regression level 2.
+regression levels are reserved for longer running regressions. 
 
-To only run some benchmarks, you can use the `TEST_REGEX` environment variable.
-For example:
-
-```
-TEST_REGEX=quantifiers make regress0
-```
-
-This runs regression tests from level 0 that have "quantifiers" in their name.
+For running regressions tests, 
+see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file.
 
 By default, each invocation of CVC4 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
@@ -35,10 +25,10 @@ To add a new regression file, add the file to git, for example:
 git add regress/regress0/testMyFunctionality.cvc
 ```
 
-Also add it to [Makefile.tests](Makefile.tests) in this directory.
+Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory.
 
 A number of regressions exist under test/regress that are not listed in
-[Makefile.tests](Makefile.tests). These are regressions that may someday be
+[CMakeLists.txt](CMakeLists.txt). These are regressions that may someday be
 included in the standard suite of tests, but are not yet included (perhaps they
 test functionality not yet supported).
 
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 4d2e828b5..30c87333e 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --fewer-preprocessing-holes
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
new file mode 100644
index 000000000..8e47c8840
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_ABV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(define-sort bv () (_ BitVec 4))
+(define-sort abv () (Array bv bv))
+
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun v1 () (_ BitVec 4))
+(declare-fun a () abv)
+(declare-fun b () abv)
+(declare-fun c () abv)
+
+(assert (not (= (select a (select b (select c v0))) (select a (select b (select c v1))))))
+
+(assert (= v0 v1))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
new file mode 100644
index 000000000..cb8ad2e55
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun g ((_ BitVec 4)) (_ BitVec 4))
+
+(assert (= (f v0) (g (f v0))))
+(assert (= (f (f v0)) (g (f v0))))
+(assert (= (f (f (f v0))) (g (f v0))))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2
index 92c7e4117..8706c51a8 100644
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ b/test/regress/regress0/bv/bool-to-bv.smt2
@@ -6,7 +6,14 @@
 (declare-fun x0 () (_ BitVec 3))
 (declare-fun b1 () Bool)
 (declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
 (assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
 (assert (= #b000 x2))
 (assert (=> b1 b2))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b3))
+(assert (not (xor b2 b2)))
+(assert (ite b2 b2 b1))
 (check-sat)
diff --git a/test/regress/regress0/bv/bv-to-bool.smt b/test/regress/regress0/bv/bv-to-bool1.smt
index ef4cec257..ef4cec257 100644
--- a/test/regress/regress0/bv/bv-to-bool.smt
+++ b/test/regress/regress0/bv/bv-to-bool1.smt
diff --git a/test/regress/regress0/bv/bv-to-bool2.smt2 b/test/regress/regress0/bv/bv-to-bool2.smt2
new file mode 100644
index 000000000..fb741733d
--- /dev/null
+++ b/test/regress/regress0/bv/bv-to-bool2.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --bv-to-bool
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () (_ BitVec 1))
+
+(assert (= (bvxor v2 v1) v1))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2
index edacdbe37..52eeedae6 100644
--- a/test/regress/regress0/quantifiers/macros-real-arg.smt2
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -3,7 +3,8 @@
 ; this will fail if type rule for APPLY_UF is made strict
 (set-logic UFLIRA)
 (declare-fun P (Int) Bool)
-(assert (forall ((x Int)) (P x)))
+(declare-fun Q (Int) Bool)
+(assert (and (forall ((x Int)) (P x)) (forall ((x Int)) (Q x))))
 (declare-fun k () Real)
 (declare-fun k2 () Int)
 (assert (or (not (P (to_int k))) (not (P k2))))
diff --git a/test/regress/regress0/strings/unsound-repl-rewrite.smt2 b/test/regress/regress0/strings/unsound-repl-rewrite.smt2
new file mode 100644
index 000000000..02e4cc0b2
--- /dev/null
+++ b/test/regress/regress0/strings/unsound-repl-rewrite.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () Int)
+(assert (not (= (str.replace "B" (str.replace "" x "A") "B") (str.replace "B" x "B"))))
+(check-sat)
diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy
index 7b96a2bf3..8203fd9cf 100644
--- a/test/regress/regress1/sygus/commutative-stream.sy
+++ b/test/regress/regress1/sygus/commutative-stream.sy
@@ -3,7 +3,7 @@
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --decision=justification
+; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification
 
 (set-logic LIA)
 
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 90d34f7c6..eeab46f99 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -1,4 +1,6 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(api_guards_black api)
+cvc4_add_unit_test_black(solver_black api)
+cvc4_add_unit_test_black(sort_black api)
+cvc4_add_unit_test_black(term_black api)
diff --git a/test/unit/api/api_guards_black.h b/test/unit/api/api_guards_black.h
deleted file mode 100644
index 777ce81f1..000000000
--- a/test/unit/api/api_guards_black.h
+++ /dev/null
@@ -1,473 +0,0 @@
-/*********************                                                        */
-/*! \file api_guards_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** 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 guards of the C++ API functions.
- **
- ** Black box testing of the guards of the C++ API functions.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class ApiGuardsBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testSolverMkBitVectorSort();
-  void testSolverMkFloatingPointSort();
-  void testSolverMkDatatypeSort();
-  void testSolverMkFunctionSort();
-  void testSolverMkPredicateSort();
-  void testSolverMkTupleSort();
-  void testSortGetDatatype();
-  void testSortInstantiate();
-  void testSortGetFunctionArity();
-  void testSortGetFunctionDomainSorts();
-  void testSortGetFunctionCodomainSort();
-  void testSortGetArrayIndexSort();
-  void testSortGetArrayElementSort();
-  void testSortGetSetElementSort();
-  void testSortGetUninterpretedSortName();
-  void testSortIsUninterpretedSortParameterized();
-  void testSortGetUninterpretedSortParamSorts();
-  void testSortGetUninterpretedSortConstructorName();
-  void testSortGetUninterpretedSortConstructorArity();
-  void testSortGetBVSize();
-  void testSortGetFPExponentSize();
-  void testSortGetFPSignificandSize();
-  void testSortGetDatatypeParamSorts();
-  void testSortGetDatatypeArity();
-  void testSortGetTupleLength();
-  void testSortGetTupleSorts();
-  void testSolverDeclareFun();
-  void testSolverDefineFun();
-  void testSolverDefineFunRec();
-  void testSolverDefineFunsRec();
-
- private:
-  Solver d_solver;
-};
-
-void ApiGuardsBlack::setUp() {}
-
-void ApiGuardsBlack::tearDown() {}
-
-void ApiGuardsBlack::testSolverMkBitVectorSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
-  TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkFloatingPointSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8));
-  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkDatatypeSort()
-{
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec));
-  DatatypeDecl throwsDtypeSpec("list");
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkFunctionSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
-      d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
-      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
-      d_solver.getIntegerSort()));
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
-                              d_solver.getIntegerSort()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
-                                            d_solver.mkUninterpretedSort("u")},
-                                           funSort2),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkPredicateSort()
-{
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
-  TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
-      CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkTupleSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatype()
-{
-  // create datatype sort, check should not fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
-  // create bv sort, check should fail
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortInstantiate()
-{
-  // instantiate parametric datatype, check should not fail
-  Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl paramDtypeSpec("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
-  paramDtypeSpec.addConstructor(paramCons);
-  paramDtypeSpec.addConstructor(paramNil);
-  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(
-      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
-  // instantiate non-parametric datatype sort, check should fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS(
-      dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
-      CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionArity()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionDomainSorts()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionCodomainSort()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetArrayIndexSort()
-{
-  Sort elementSort = d_solver.mkBitVectorSort(32);
-  Sort indexSort = d_solver.mkBitVectorSort(32);
-  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
-  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort());
-  TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetArrayElementSort()
-{
-  Sort elementSort = d_solver.mkBitVectorSort(32);
-  Sort indexSort = d_solver.mkBitVectorSort(32);
-  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
-  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort());
-  TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetSetElementSort()
-{
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortName()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortIsUninterpretedSortParameterized()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortParamSorts()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortConstructorName()
-{
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortConstructorArity()
-{
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetBVSize()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFPExponentSize()
-{
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFPSignificandSize()
-{
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatypeParamSorts()
-{
-  // create parametric datatype, check should not fail
-  Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl paramDtypeSpec("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
-  paramDtypeSpec.addConstructor(paramCons);
-  paramDtypeSpec.addConstructor(paramNil);
-  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
-  // create non-parametric datatype sort, check should fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatypeArity()
-{
-  // create datatype sort, check should not fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
-  // create bv sort, check should fail
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetTupleLength()
-{
-  Sort tupleSort = d_solver.mkTupleSort(
-      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
-  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetTupleSorts()
-{
-  Sort tupleSort = d_solver.mkTupleSort(
-      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
-  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDeclareFun()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
-  TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFun()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFunRec()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFunsRec()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term b4 = d_solver.mkBoundVar("b4", uSort);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term v4 = d_solver.mkVar("v4", uSort);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
-  TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
-      CVC4ApiException&);
-}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
new file mode 100644
index 000000000..538899a0f
--- /dev/null
+++ b/test/unit/api/solver_black.h
@@ -0,0 +1,230 @@
+/*********************                                                        */
+/*! \file api_guards_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** 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 guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class SolverBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testMkBitVectorSort();
+  void testMkFloatingPointSort();
+  void testMkDatatypeSort();
+  void testMkFunctionSort();
+  void testMkPredicateSort();
+  void testMkTupleSort();
+  void testDeclareFun();
+  void testDefineFun();
+  void testDefineFunRec();
+  void testDefineFunsRec();
+
+ private:
+  Solver d_solver;
+};
+
+void SolverBlack::setUp() {}
+
+void SolverBlack::tearDown() {}
+
+void SolverBlack::testMkBitVectorSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
+  TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&);
+}
+
+void SolverBlack::testMkFloatingPointSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8));
+  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&);
+}
+
+void SolverBlack::testMkDatatypeSort()
+{
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec));
+  DatatypeDecl throwsDtypeSpec("list");
+  TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&);
+}
+
+void SolverBlack::testMkFunctionSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
+      d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
+      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
+      d_solver.getIntegerSort()));
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(
+      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
+                              d_solver.getIntegerSort()),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
+                                            d_solver.mkUninterpretedSort("u")},
+                                           funSort2),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testMkPredicateSort()
+{
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
+  TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(
+      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
+      CVC4ApiException&);
+}
+
+void SolverBlack::testMkTupleSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testDeclareFun()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
+  TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFun()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1));
+  TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFunRec()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1));
+  TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFunsRec()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term b4 = d_solver.mkBoundVar("b4", uSort);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term v4 = d_solver.mkVar("v4", uSort);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
+  TS_ASSERT_THROWS(
+      d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
+      CVC4ApiException&);
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
new file mode 100644
index 000000000..d9337e627
--- /dev/null
+++ b/test/unit/api/sort_black.h
@@ -0,0 +1,279 @@
+/*********************                                                        */
+/*! \file api_guards_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** 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 guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class SortBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testGetDatatype();
+  void testInstantiate();
+  void testGetFunctionArity();
+  void testGetFunctionDomainSorts();
+  void testGetFunctionCodomainSort();
+  void testGetArrayIndexSort();
+  void testGetArrayElementSort();
+  void testGetSetElementSort();
+  void testGetUninterpretedSortName();
+  void testIsUninterpretedSortParameterized();
+  void testGetUninterpretedSortParamSorts();
+  void testGetUninterpretedSortConstructorName();
+  void testGetUninterpretedSortConstructorArity();
+  void testGetBVSize();
+  void testGetFPExponentSize();
+  void testGetFPSignificandSize();
+  void testGetDatatypeParamSorts();
+  void testGetDatatypeArity();
+  void testGetTupleLength();
+  void testGetTupleSorts();
+
+ private:
+  Solver d_solver;
+};
+
+void SortBlack::setUp() {}
+
+void SortBlack::tearDown() {}
+
+void SortBlack::testGetDatatype()
+{
+  // create datatype sort, check should not fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
+  // create bv sort, check should fail
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
+}
+
+void SortBlack::testInstantiate()
+{
+  // instantiate parametric datatype, check should not fail
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl paramDtypeSpec("paramlist", sort);
+  DatatypeConstructorDecl paramCons("cons");
+  DatatypeConstructorDecl paramNil("nil");
+  DatatypeSelectorDecl paramHead("head", sort);
+  paramCons.addSelector(paramHead);
+  paramDtypeSpec.addConstructor(paramCons);
+  paramDtypeSpec.addConstructor(paramNil);
+  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(
+      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
+  // instantiate non-parametric datatype sort, check should fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS(
+      dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
+      CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionArity()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionDomainSorts()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionCodomainSort()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetArrayIndexSort()
+{
+  Sort elementSort = d_solver.mkBitVectorSort(32);
+  Sort indexSort = d_solver.mkBitVectorSort(32);
+  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort());
+  TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetArrayElementSort()
+{
+  Sort elementSort = d_solver.mkBitVectorSort(32);
+  Sort indexSort = d_solver.mkBitVectorSort(32);
+  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort());
+  TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetSetElementSort()
+{
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortName()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&);
+}
+
+void SortBlack::testIsUninterpretedSortParameterized()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(),
+                   CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortParamSorts()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortConstructorName()
+{
+  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortConstructorArity()
+{
+  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetBVSize()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFPExponentSize()
+{
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFPSignificandSize()
+{
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetDatatypeParamSorts()
+{
+  // create parametric datatype, check should not fail
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl paramDtypeSpec("paramlist", sort);
+  DatatypeConstructorDecl paramCons("cons");
+  DatatypeConstructorDecl paramNil("nil");
+  DatatypeSelectorDecl paramHead("head", sort);
+  paramCons.addSelector(paramHead);
+  paramDtypeSpec.addConstructor(paramCons);
+  paramDtypeSpec.addConstructor(paramNil);
+  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
+  // create non-parametric datatype sort, check should fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetDatatypeArity()
+{
+  // create datatype sort, check should not fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
+  // create bv sort, check should fail
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetTupleLength()
+{
+  Sort tupleSort = d_solver.mkTupleSort(
+      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&);
+}
+
+void SortBlack::testGetTupleSorts()
+{
+  Sort tupleSort = d_solver.mkTupleSort(
+      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
+}
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;
+};
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 87aef3704..42ac2cdd9 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -604,6 +604,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              b);
     repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
     sameNormalForm(repl_repl, repl);
+
+    // Different normal forms for:
+    //
+    // (str.replace "B" (str.replace "" x "A") "B")
+    //
+    // (str.replace "B" x "B")
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             b,
+                             d_nm->mkNode(kind::STRING_STRREPL, empty, x, a),
+                             b);
+    repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
+    differentNormalForms(repl_repl, repl);
   }
 
   void testRewriteContains()