diff options
| -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 |