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 3f419c66de9793e3655d17ad9a0dd8475c1a09df..46570df48046630be743ae0f1d0a9110eb333174 100644 (file)
--- 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 edf49b502eab106647d3610799f3cd72d21d4514..d455bb85b39676f509a2556752e816795eb6b300 100644 (file)
--- 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 (file)
index 0000000..a1e7eb7
--- /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)