Fix strings rewriter for non-standard re range (#6570)

Fixes #6561.

Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 1577a5625723d3fba38a2f57875b1905ecf482fb..e827e87d349d29916f5056a3a074728a7da5218d 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1129,6 +1129,17 @@ Node SequencesRewriter::rewriteDifferenceRegExp(TNode node)
 Node SequencesRewriter::rewriteRangeRegExp(TNode node)
 {
   Assert(node.getKind() == REGEXP_RANGE);
+  unsigned ch[2];
+  for (size_t i = 0; i < 2; ++i)
+  {
+    if (!node[i].isConst() || node[i].getConst<String>().size() != 1)
+    {
+      // not applied to characters, it is not handled
+      return node;
+    }
+    ch[i] = node[i].getConst<String>().front();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   if (node[0] == node[1])
   {
@@ -1137,18 +1148,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node)
     return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE);
   }
 
-  bool appliedCh = true;
-  unsigned ch[2];
-  for (size_t i = 0; i < 2; ++i)
-  {
-    if (node[i].isConst() || node[i].getConst<String>().size() != 1)
-    {
-      appliedCh = false;
-      break;
-    }
-    ch[i] = node[i].getConst<String>().front();
-  }
-  if (appliedCh && ch[0] > ch[1])
+  if (ch[0] > ch[1])
   {
     // re.range( "B", "A" ) ---> re.none
     Node retNode = nm->mkNode(REGEXP_EMPTY, {});