From e2ced5d1e84ea1562eae907fd2b245bae4593406 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 16 Mar 2020 11:22:15 -0700 Subject: Issue 4077: Add unit test to reproduce issue. (#4107) This adds the unit test reported in issue #4077. The issue was fixed in #4081. --- test/unit/api/solver_black.h | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 6d6557449..27f5aca12 100644 --- 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 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}); +} -- cgit v1.2.3