1 files changed, 42 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 33ee51007..a82807b3b 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -84,6 +84,12 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFunRec();
   void testDefineFunsRec();
 
+  void testPush1();
+  void testPush2();
+  void testPop1();
+  void testPop2();
+  void testPop3();
+
   void testSetInfo();
   void testSetLogic();
   void testSetOption();
@@ -879,6 +885,42 @@ void SolverBlack::testDefineFunsRec()
       CVC4ApiException&);
 }
 
+void SolverBlack::testPush1()
+{
+  d_solver->setOption("incremental", "true");
+  TS_ASSERT_THROWS_NOTHING(d_solver->push(1));
+  TS_ASSERT_THROWS(d_solver->setOption("incremental", "false"),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->setOption("incremental", "true"),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testPush2()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS(d_solver->push(1), CVC4ApiException&);
+}
+
+void SolverBlack::testPop1()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
+}
+
+void SolverBlack::testPop2()
+{
+  d_solver->setOption("incremental", "true");
+  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
+}
+
+void SolverBlack::testPop3()
+{
+  d_solver->setOption("incremental", "true");
+  TS_ASSERT_THROWS_NOTHING(d_solver->push(1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->pop(1));
+  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
+}
+
 void SolverBlack::testSetInfo()
 {
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);