diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-11-03 14:52:36 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-03 21:52:36 +0000 |
| commit | 79cbac66b3676cfcaeb9739ad046084f6328ac74 (patch) | |
| tree | b2cffeb9ef2657fd273a0f3d8db0aedc71515ef2 | |
| parent | 690a3926569a29217df5000cfb673cc407ada356 (diff) | |
Add unit test to cover previous failure with second solver instance. (#7565)
Fixes #5893.
| -rw-r--r-- | test/unit/api/solver_black.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 8435a63be..25abdd108 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -2557,5 +2557,19 @@ TEST_F(TestApiBlackSolver, issue7000) ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); } +TEST_F(TestApiBlackSolver, issue5893) +{ + Solver slv; + Sort bvsort4 = d_solver.mkBitVectorSort(4); + Sort bvsort8 = d_solver.mkBitVectorSort(8); + Sort arrsort = d_solver.mkArraySort(bvsort4, bvsort8); + Term arr = d_solver.mkConst(arrsort, "arr"); + Term idx = d_solver.mkConst(bvsort4, "idx"); + Term ten = d_solver.mkBitVector(8, "10", 10); + Term sel = d_solver.mkTerm(SELECT, arr, idx); + Term distinct = d_solver.mkTerm(DISTINCT, sel, ten); + ASSERT_NO_FATAL_FAILURE(distinct.getOp()); +} + } // namespace test } // namespace cvc5 |