Add missing tests for some corners of the API (#8688)

This PR adds a bunch of unit tests for some not yet covered corners of the API.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e6e0686614be0aa22a94d107a9a55e9e5a27fe54..b5f0d463a12b57c122b9d298235170a080cf240f 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1915,6 +1915,9 @@ size_t Op::getNumIndicesHelper() const
     case TUPLE_PROJECT:
       size = d_node->getConst<internal::TupleProjectOp>().getIndices().size();
       break;
+    case TABLE_PROJECT:
+      size = d_node->getConst<internal::TableProjectOp>().getIndices().size();
+      break;
     default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k);
   }
   return size;
@@ -4208,6 +4211,11 @@ bool Datatype::const_iterator::operator!=(
 
 bool Datatype::isNullHelper() const { return d_dtype == nullptr; }
 
+std::ostream& operator<<(std::ostream& out, const Datatype& dtype)
+{
+  return out << dtype.toString();
+}
+
 /* -------------------------------------------------------------------------- */
 /* Grammar                                                                    */
 /* -------------------------------------------------------------------------- */

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 0743bc2192699ea766ea2072a5f35a2c8cdf5ae2..5af31b074f3a2b35761bc61fe12798d7b3a3b32e 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2377,21 +2377,26 @@ cdef class Solver:
             diffi[termk] = termv
         return diffi
 
-    def getValue(self, Term t):
+    def getValue(self, term_or_list):
         """
-            Get the value of the given term in the current model.
+            Get the value of the given term or list of terms in the current
+            model.
 
             SMT-LIB:
 
             .. code-block:: smtlib
 
-                ( get-value ( <term> ) )
+                ( get-value ( <term>* ) )
 
-            :param term: The term for which the value is queried.
-            :return: The value of the given term.
+            :param term_or_list: The term or list of terms for which the value
+                                 is queried.
+            :return: The value or list of values of the given term or list of
+                     terms.
         """
+        if isinstance(term_or_list, list):
+            return [self.getValue(t) for t in term_or_list]
         cdef Term term = Term(self)
-        term.cterm = self.csolver.getValue(t.cterm)
+        term.cterm = self.csolver.getValue((<Term> term_or_list).cterm)
         return term
 
     def getModelDomainElements(self, Sort s):

diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index 2a66a3b55d0163ecf48c75cb6a5fa08f96d380ea..f810037f3312d703341d5ccc549b3b52ca4bb49c 100644 (file)
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -61,6 +61,8 @@ TEST_F(TestApiBlackDatatype, isNull)
   cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
+  ASSERT_EQ(dtypeSpec.getNumConstructors(), 1);
+  ASSERT_FALSE(dtypeSpec.isParametric());
   Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
   d = listSort.getDatatype();
   consConstr = d[0];
@@ -72,6 +74,55 @@ TEST_F(TestApiBlackDatatype, isNull)
   ASSERT_FALSE(d.isNull());
   ASSERT_FALSE(consConstr.isNull());
   ASSERT_FALSE(sel.isNull());
+
+  {
+    std::stringstream ss;
+    ss << cons;
+    ASSERT_EQ(ss.str(), cons.toString());
+  }
+  {
+    std::stringstream ss;
+    ss << sel;
+    ASSERT_EQ(ss.str(), sel.toString());
+  }
+  {
+    std::stringstream ss;
+    ss << consConstr;
+    ASSERT_EQ(ss.str(), consConstr.toString());
+  }
+  {
+    std::stringstream ss;
+    ss << d;
+    ASSERT_EQ(ss.str(), d.toString());
+  }
+
+  {
+    Datatype::const_iterator it;
+    it = d.begin();
+    ASSERT_TRUE(it != d.end());
+    ASSERT_FALSE(it->isNull());
+    ASSERT_FALSE((*it).isNull());
+    auto tmp = it;
+    tmp++;
+    ASSERT_EQ(tmp, d.end());
+    tmp = it;
+    ++tmp;
+    ASSERT_EQ(tmp, d.end());
+  }
+
+  {
+    DatatypeConstructor::const_iterator it;
+    it = consConstr.begin();
+    ASSERT_TRUE(it != consConstr.end());
+    ASSERT_FALSE(it->isNull());
+    ASSERT_FALSE((*it).isNull());
+    auto tmp = it;
+    tmp++;
+    ASSERT_EQ(tmp, consConstr.end());
+    tmp = it;
+    ++tmp;
+    ASSERT_EQ(tmp, consConstr.end());
+  }
 }
 
 TEST_F(TestApiBlackDatatype, mkDatatypeSorts)

diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp
index 5340f0f7a174e95dbf71c9330325e9cef12ee599..810f301f0ae12c361f5d4b8f5e543a2275fa463a 100644 (file)
--- a/test/unit/api/cpp/grammar_black.cpp
+++ b/test/unit/api/cpp/grammar_black.cpp
@@ -23,6 +23,22 @@ class TestApiBlackGrammar : public TestApi
 {
 };
 
+TEST_F(TestApiBlackGrammar, toString)
+{
+  d_solver.setOption("sygus", "true");
+  Sort boolean = d_solver.getBooleanSort();
+  Term start = d_solver.mkVar(boolean);
+  Grammar g;
+  g = d_solver.mkGrammar({}, {start});
+  g.addRule(start, d_solver.mkBoolean(false));
+
+  {
+    std::stringstream ss;
+    ss << g;
+    ASSERT_EQ(ss.str(), g.toString());
+  }
+}
+
 TEST_F(TestApiBlackGrammar, addRule)
 {
   d_solver.setOption("sygus", "true");

diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp
index b9c059602289a57e38cb19ea0d41c630332f4153..498c18c001180ac1c1d74e3162b2ab72a0964d9d 100644 (file)
--- a/test/unit/api/cpp/op_black.cpp
+++ b/test/unit/api/cpp/op_black.cpp
@@ -102,6 +102,9 @@ TEST_F(TestApiBlackOp, getNumIndices)
   std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
   Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
   ASSERT_EQ(indices.size(), tupleProject.getNumIndices());
+
+  Op tableProject = d_solver.mkOp(TABLE_PROJECT, indices);
+  ASSERT_EQ(indices.size(), tableProject.getNumIndices());
 }
 
 TEST_F(TestApiBlackOp, subscriptOperator)
@@ -122,6 +125,7 @@ TEST_F(TestApiBlackOp, subscriptOperator)
   Op iand = d_solver.mkOp(IAND, {11});
   Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, {12});
   Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, {13});
+  Op regexpRepeat = d_solver.mkOp(REGEXP_REPEAT, {14});
 
   ASSERT_EQ(4, divisible[0].getUInt32Value());
   ASSERT_EQ(5, bvRepeat[0].getUInt32Value());
@@ -133,6 +137,7 @@ TEST_F(TestApiBlackOp, subscriptOperator)
   ASSERT_EQ(11, iand[0].getUInt32Value());
   ASSERT_EQ(12, fpToUbv[0].getUInt32Value());
   ASSERT_EQ(13, fpToSbv[0].getUInt32Value());
+  ASSERT_EQ(14, regexpRepeat[0].getUInt32Value());
 
   // Operators with 2 indices
   Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, {1, 0});

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 6fbc2f46f5b433ba26311d046ae0ac2526ceba1f..a25669474d208177df9054dd7c1a4e66b458e5b3 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -91,6 +91,15 @@ TEST_F(TestApiBlackSolver, recoverableException)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
   ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException);
+  
+  try {
+    d_solver.getValue(x);
+  }
+  catch (const CVC5ApiRecoverableException& e)
+  {
+    ASSERT_NO_THROW(e.what());
+    ASSERT_NO_THROW(e.getMessage());
+  }
 }
 
 TEST_F(TestApiBlackSolver, supportsFloatingPoint)
@@ -720,6 +729,8 @@ TEST_F(TestApiBlackSolver, mkString)
             "\"asdf\\u{5c}nasdf\"");
   ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
             "\"asdf\\u{5c}nasdf\"");
+  std::wstring s;
+  ASSERT_EQ(d_solver.mkString(s).getStringValue(), s);
 }
 
 TEST_F(TestApiBlackSolver, mkTerm)
@@ -1339,6 +1350,16 @@ TEST_F(TestApiBlackSolver, uFIteration)
   }
 }
 
+TEST_F(TestApiBlackSolver, getAssertions)
+{
+  Term a = d_solver.mkConst(d_solver.getBooleanSort(), "a");
+  Term b = d_solver.mkConst(d_solver.getBooleanSort(), "b");
+  d_solver.assertFormula(a);
+  d_solver.assertFormula(b);
+  std::vector<Term> asserts{a, b};
+  ASSERT_EQ(d_solver.getAssertions(), asserts);
+}
+
 TEST_F(TestApiBlackSolver, getInfo)
 {
   ASSERT_NO_THROW(d_solver.getInfo("name"));
@@ -1665,7 +1686,7 @@ TEST_F(TestApiBlackSolver, getDriverOptions)
   ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf());
   ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf());
 }
-  
+
 TEST_F(TestApiBlackSolver, getStatistics)
 {
   ASSERT_NO_THROW(cvc5::Stat());
@@ -1943,6 +1964,14 @@ TEST_F(TestApiBlackSolver, getValue3)
   ASSERT_NO_THROW(d_solver.getValue(sum));
   ASSERT_NO_THROW(d_solver.getValue(p_f_y));
 
+  std::vector<Term> a;
+  ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(x)));
+  ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(y)));
+  ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(z)));
+  std::vector<Term> b;
+  ASSERT_NO_THROW(b = d_solver.getValue({x,y,z}));
+  ASSERT_EQ(a,b);
+
   Solver slv;
   ASSERT_THROW(slv.getValue(x), CVC5ApiException);
 }

diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp
index 35911b4e8a93a919552cd7f04cb404958426f7a0..93f229f17ce4de8e5fd04dc49c83f9b3b2bd1fed 100644 (file)
--- a/test/unit/api/cpp/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
@@ -50,5 +50,12 @@ TEST_F(TestApiWhiteSolver, getOp)
   ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 
+TEST_F(TestApiWhiteSolver, printStatisticsSafe)
+{
+  testing::internal::CaptureStdout();
+  d_solver.printStatisticsSafe(STDOUT_FILENO);
+  testing::internal::GetCapturedStdout();
+}
+
 }  // namespace test
 }  // namespace cvc5::internal

diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp
index 025e62772ba9431f7ccadc3b18841b2210cceb09..c902fbbc9479084127ec06fa317a9555af9d3cc2 100644 (file)
--- a/test/unit/api/cpp/synth_result_black.cpp
+++ b/test/unit/api/cpp/synth_result_black.cpp
@@ -44,6 +44,11 @@ TEST_F(TestApiBlackSynthResult, hasSolution)
   ASSERT_FALSE(res.hasNoSolution());
   ASSERT_FALSE(res.isUnknown());
   ASSERT_EQ(res.toString(), "(SOLUTION)");
+  {
+    std::stringstream ss;
+    ss << res;
+    ASSERT_EQ(res.toString(), ss.str());
+  }
 }
 
 TEST_F(TestApiBlackSynthResult, hasNoSolution)

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 93a5b73f6874cbd650b31a4f38ae9508d9b5f062..defcc935e40be37963e6727d19e1dcf9e2d9a107 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -667,6 +667,14 @@ TEST_F(TestApiBlackTerm, termChildren)
   Term tnull;
   ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException);
 
+  Term::const_iterator it;
+  it = t1.begin();
+  ASSERT_TRUE((*it).isIntegerValue());
+  it++;
+  ASSERT_TRUE((*it).isIntegerValue());
+  ++it;
+  ASSERT_EQ(it, t1.end());
+
   // apply term f(2)
   Sort intSort = d_solver.getIntegerSort();
   Sort fsort = d_solver.mkFunctionSort({intSort}, intSort);
@@ -1159,6 +1167,16 @@ TEST_F(TestApiBlackTerm, termScopedToString)
   ASSERT_EQ(x.toString(), "x");
 }
 
-TEST_F(TestApiBlackTerm, toString) { ASSERT_NO_THROW(Term().toString()); }
+TEST_F(TestApiBlackTerm, toString) {
+  ASSERT_NO_THROW(Term().toString());
+
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+  std::stringstream ss;
+
+  ss << std::vector<Term>{x, x};
+  ss << std::set<Term>{x, x};
+  ss << std::unordered_set<Term>{x, x};
+}
 }  // namespace test
 }  // namespace cvc5::internal

diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index 7113e9db6fe76edb49499073cb9e5040d5f9097a..224b051c437e851ac027854f63cba7c5b4d84876 100644 (file)
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -140,6 +140,7 @@ class OpTest
     Op iand = d_solver.mkOp(IAND, 11);
     Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
     Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+    Op regexpRepeat = d_solver.mkOp(REGEXP_REPEAT, 14);
 
     assertEquals(4, divisible.get(0).getIntegerValue().intValue());
     assertEquals(5, bvRepeat.get(0).getIntegerValue().intValue());
@@ -151,6 +152,7 @@ class OpTest
     assertEquals(11, iand.get(0).getIntegerValue().intValue());
     assertEquals(12, fpToUbv.get(0).getIntegerValue().intValue());
     assertEquals(13, fpToSbv.get(0).getIntegerValue().intValue());
+    assertEquals(14, regexpRepeat.get(0).getIntegerValue().intValue());
 
     // Operators with 2 indices
     Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);

diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp
index 1c2cb89cec9ca4ea01f5d787292204bfb711917a..a041db700da9112dad0bdd12232121d55e836514 100644 (file)
--- a/test/unit/api/java/UncoveredTest.cpp
+++ b/test/unit/api/java/UncoveredTest.cpp
@@ -23,11 +23,49 @@ class TestApiBlackUncovered : public TestApi
 {
 };
 
+TEST_F(TestApiBlackUncovered, exception_getmessage)
+{
+  d_solver.setOption("produce-models", "true");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+
+  ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException);
+  
+  try {
+    d_solver.getValue(x);
+  }
+  catch (const CVC5ApiRecoverableException& e)
+  {
+    ASSERT_NO_THROW(e.getMessage());
+  }
+}
+
 TEST_F(TestApiBlackUncovered, streaming_operators)
 {
-    std::stringstream ss;
-    ss << cvc5::modes::LearnedLitType::PREPROCESS;
-    ss << cvc5::SynthResult();
+  std::stringstream ss;
+  ss << cvc5::modes::LearnedLitType::PREPROCESS;
+  ss << cvc5::Result();
+  ss << cvc5::Op();
+  ss << cvc5::SynthResult();
+
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+
+  ss << std::vector<Term>{x, x};
+  ss << std::set<Term>{x, x};
+  ss << std::unordered_set<Term>{x, x};
+}
+
+TEST_F(TestApiBlackUncovered, hash)
+{
+    std::hash<Op>()(Op());
+    std::hash<Sort>()(Sort());
+}
+
+TEST_F(TestApiBlackUncovered, isOutputOn)
+{
+  d_solver.isOutputOn("inst");
+  d_solver.getOutput("inst");
 }
 
 TEST_F(TestApiBlackUncovered, Options)

diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py
index 00af24c4f8d72c2eeb963db880f8cf370d63b329..4ba60792654e63849d37825badba15fb129ec2f0 100644 (file)
--- a/test/unit/api/python/test_op.py
+++ b/test/unit/api/python/test_op.py
@@ -105,6 +105,9 @@ def test_get_num_indices(solver):
     tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices)
     assert len(indices) == tuple_project_op.getNumIndices()
 
+    table_project_op = solver.mkOp(Kind.TABLE_PROJECT, *indices)
+    assert len(indices) == table_project_op.getNumIndices()
+
 
 def test_subscript_operator(solver):
     # Operators with 0 indices
@@ -124,6 +127,7 @@ def test_subscript_operator(solver):
     iand = solver.mkOp(Kind.IAND, 11)
     floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 12)
     floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13)
+    regexp_repeat = solver.mkOp(Kind.REGEXP_REPEAT, 14)
 
     assert 4 == divisible[0].getIntegerValue()
     assert 5 == bitvector_repeat[0].getIntegerValue()
@@ -135,6 +139,7 @@ def test_subscript_operator(solver):
     assert 11 == iand[0].getIntegerValue()
     assert 12 == floatingpoint_to_ubv[0].getIntegerValue()
     assert 13 == floatingopint_to_sbv[0].getIntegerValue()
+    assert 14 == regexp_repeat[0].getIntegerValue()
 
     # Operators with 2 indices
     bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 0)

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 736111d96fc09a9b828abfba03a2b866d03e4fd8..3939f2d09503102c005fabb5fac095d329f1adae 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -703,6 +703,8 @@ def test_mk_string(solver):
     str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\""
     str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\
             "\"asdf\\u{5c}nasdf\""
+    s = ""
+    assert solver.mkString(s).getStringValue() == s
 
 
 def test_mk_term(solver):
@@ -1127,6 +1129,15 @@ def test_uf_iteration(solver):
         idx = idx + 1
 
 
+def test_get_assertions(solver):
+    a = solver.mkConst(solver.getBooleanSort(), 'a')
+    b = solver.mkConst(solver.getBooleanSort(), 'b')
+    solver.assertFormula(a)
+    solver.assertFormula(b)
+    asserts = [a,b]
+    assert solver.getAssertions() == asserts
+
+
 def test_get_info(solver):
     solver.getInfo("name")
     with pytest.raises(RuntimeError):
@@ -1403,6 +1414,10 @@ def test_get_value3(solver):
     solver.getValue(summ)
     solver.getValue(p_f_y)
 
+    a = [solver.getValue(x), solver.getValue(y), solver.getValue(z)]
+    b = solver.getValue([x,y,z])
+    assert a == b
+
     slv = cvc5.Solver()
     with pytest.raises(RuntimeError):
         slv.getValue(x)

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index f166ecd0a9f62498404b76af76b13a03823abe41..c9db1cb9a5b7f7af13a3949658dc3ed817113e09 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -1313,7 +1313,6 @@ def test_get_cardinality_constraint(solver):
     nullt.isCardinalityConstraint()
 
 
-
 def test_term_scoped_to_string(solver):
     intsort = solver.getIntegerSort()
     x = solver.mkConst(intsort, "x")

diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp
index c64887b0f3e92d5280dfcace2ea1b9ba1b831ae9..fbeef181e1aeaa1604dba7eda04128827a79b130 100644 (file)
--- a/test/unit/api/python/test_uncovered.cpp
+++ b/test/unit/api/python/test_uncovered.cpp
@@ -23,11 +23,53 @@ class TestApiBlackUncovered : public TestApi
 {
 };
 
+TEST_F(TestApiBlackUncovered, exception_getmessage)
+{
+  d_solver.setOption("produce-models", "true");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+
+  ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException);
+  
+  try {
+    d_solver.getValue(x);
+  }
+  catch (const CVC5ApiRecoverableException& e)
+  {
+    ASSERT_NO_THROW(e.getMessage());
+  }
+}
+
 TEST_F(TestApiBlackUncovered, streaming_operators)
 {
-    std::stringstream ss;
-    ss << cvc5::modes::LearnedLitType::PREPROCESS;
-    ss << cvc5::SynthResult();
+  std::stringstream ss;
+  ss << cvc5::modes::LearnedLitType::PREPROCESS;
+  ss << cvc5::Result();
+  ss << cvc5::Op();
+  ss << cvc5::SynthResult();
+
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+
+  ss << std::vector<Term>{x, x};
+  ss << std::set<Term>{x, x};
+  ss << std::unordered_set<Term>{x, x};
+}
+
+TEST_F(TestApiBlackUncovered, getValue)
+{
+  d_solver.setOption("produce-models", "true");
+  Sort boolsort = d_solver.getBooleanSort();
+  Term b = d_solver.mkConst(boolsort, "b");
+  d_solver.assertFormula(b);
+  d_solver.checkSat();
+  d_solver.getValue({b, b, b});
+}
+
+TEST_F(TestApiBlackUncovered, isOutputOn)
+{
+  d_solver.isOutputOn("inst");
+  d_solver.getOutput("inst");
 }
 
 TEST_F(TestApiBlackUncovered, Options)