From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 3 Nov 2021 21:52:36 +0000 (-0700)
Subject: Add unit test to cover previous failure with second solver instance. (#7565)
X-Git-Tag: cvc5-1.0.0~898
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=79cbac66b3676cfcaeb9739ad046084f6328ac74;p=cvc5.git

Add unit test to cover previous failure with second solver instance. (#7565)

Fixes #5893.
---

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