From 79cbac66b3676cfcaeb9739ad046084f6328ac74 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 3 Nov 2021 14:52:36 -0700 Subject: [PATCH] Add unit test to cover previous failure with second solver instance. (#7565) Fixes #5893. --- test/unit/api/solver_black.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) 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 -- 2.30.2