From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Mar 2022 21:42:39 +0000 (-0500)
Subject: Add unit test involving seq concat term (#8257)
X-Git-Tag: cvc5-1.0.0~251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27113b19f92c94047521c46c882fe74b4d063ccc;p=cvc5.git

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.
---

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;