Fix cases of ITE within regular expressions (#6783)

Fixes #6776.

Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.

That benchmark now gives:

(error "Regular expression variables are not supported.")

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index 3d4a2d143..be1646403 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -364,6 +364,10 @@ bool RegExpEntail::isConstRegExp(TNode t)
           }
         }
       }
+      else if (ck == ITE)
+      {
+        return false;
+      }
       else if (cur.isVar())
       {
         return false;