From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Feb 2021 14:08:57 +0000 (-0600)
Subject: Fix spurious assertion failure in regexp normalization (#5852)
X-Git-Tag: cvc5-1.0.0~2288
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3f05d5c25facaf0c34ee79faed060bda3f61a8d;p=cvc5.git

Fix spurious assertion failure in regexp normalization (#5852)

Fixes #5816.
---

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 3f419c66d..46570df48 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -664,7 +664,8 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
   switch (r.getKind())
   {
     case REGEXP_EMPTY:
-    case REGEXP_SIGMA: break;
+    case REGEXP_SIGMA:
+    case REGEXP_RANGE: break;
     case STRING_TO_REGEXP:
     {
       if (!r[0].isConst())
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index edf49b502..d455bb85b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1114,6 +1114,7 @@ set(regress_0_tests
   regress0/strings/issue5745-eager-pp.smt2
   regress0/strings/issue5767-eager-pp.smt2
   regress0/strings/issue5771-eager-pp.smt2
+  regress0/strings/issue5816-re-kind.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue5816-re-kind.smt2 b/test/regress/regress0/strings/issue5816-re-kind.smt2
new file mode 100644
index 000000000..a1e7eb7f4
--- /dev/null
+++ b/test/regress/regress0/strings/issue5816-re-kind.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x String)
+(declare-const x8 String)
+(assert (str.in_re x8 (re.++ (str.to_re x) (re.range "a" "u"))))
+(check-sat)