diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-16 11:22:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-16 11:22:15 -0700 |
commit | e2ced5d1e84ea1562eae907fd2b245bae4593406 (patch) | |
tree | 8bbddc24d6f58e5b2484cd0fe58570a983b3fe80 | |
parent | 33f77f7e95575cbaf5249042fa83d7b0d0650ce0 (diff) |
Issue 4077: Add unit test to reproduce issue. (#4107)
This adds the unit test reported in issue #4077.
The issue was fixed in #4081.
-rw-r--r-- | test/unit/api/solver_black.h | 17 |
1 files changed, 17 insertions, 0 deletions
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<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}); +} |