From 90d19f7cdbaf41e389bdcbd099471f658a35ce98 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Jun 2021 22:50:29 -0500
Subject: [PATCH] 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.")
---
 src/theory/strings/regexp_entail.cpp | 4 ++++
 1 file changed, 4 insertions(+)

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;
-- 
2.30.2