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

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index 3d4a2d1437ae8c6020adc7e68991e7296bf5b4bb..be164640302de4fd241653ad64cc03214c860c4f 100644 (file)
--- 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;