From 27113b19f92c94047521c46c882fe74b4d063ccc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Mar 2022 16:42:39 -0500 Subject: [PATCH] Add unit test involving seq concat term (#8257) On closer inspection, the initial version of the unit test has a type error, where an incorrect concatentation term is constructed. Adds the updated test. Fixes cvc5/cvc5-projects#423. --- test/unit/api/cpp/solver_black.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index b07b3eaa7..9545c4fb0 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3146,6 +3146,25 @@ TEST_F(TestApiBlackSolver, proj_issue422) slv.push(4); } +TEST_F(TestApiBlackSolver, proj_issue423) +{ + Solver slv; + slv.setOption("produce-models", "true"); + slv.setOption("produce-difficulty", "true"); + Sort s2 = slv.getRealSort(); + Sort s3 = slv.mkSequenceSort(s2); + Term t2; + { + t2 = slv.mkEmptySequence(s3.getSequenceElementSort()); + } + Term t22 = slv.mkReal("119605652059157009"); + Term t32 = slv.mkTerm(Kind::SEQ_UNIT, {t22}); + Term t43 = slv.mkTerm(Kind::SEQ_CONCAT, {t2, t32}); + Term t51 = slv.mkTerm(Kind::DISTINCT, {t32, t32}); + slv.checkSat(); + slv.blockModelValues({t51, t43}); +} + TEST_F(TestApiBlackSolver, projIssue431) { Solver slv; -- 2.30.2