Issue 4077: Add unit test to reproduce issue. (#4107)

This adds the unit test reported in issue #4077.
The issue was fixed in #4081.

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 6d65574490c3bae2b37e6d3543441a6ce28e1c40..27f5aca12b6c2de4848c0f8e27655dc6504656a8 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -104,6 +104,8 @@ class SolverBlack : public CxxTest::TestSuite
   void testSetLogic();
   void testSetOption();
 
+  void testResetAssertions();
+
  private:
   std::unique_ptr<Solver> d_solver;
 };
@@ -1212,3 +1214,18 @@ void SolverBlack::testSetOption()
   TS_ASSERT_THROWS(d_solver->setOption("bv-sat-solver", "minisat"),
                    CVC4ApiException&);
 }
+
+void SolverBlack::testResetAssertions()
+{
+  d_solver->setOption("incremental", "true");
+
+  Sort bvSort = d_solver->mkBitVectorSort(4);
+  Term one = d_solver->mkBitVector(4, 1);
+  Term x = d_solver->mkConst(bvSort, "x");
+  Term ule = d_solver->mkTerm(BITVECTOR_ULE, x, one);
+  Term srem = d_solver->mkTerm(BITVECTOR_SREM, one, x);
+  d_solver->push(4);
+  Term slt = d_solver->mkTerm(BITVECTOR_SLT, srem, one);
+  d_solver->resetAssertions();
+  d_solver->checkSatAssuming({slt, ule});
+}