From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Jun 2021 03:50:29 +0000 (-0500)
Subject: Fix cases of ITE within regular expressions (#6783)
X-Git-Tag: cvc5-1.0.0~1575
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90d19f7cdbaf41e389bdcbd099471f658a35ce98;p=cvc5.git

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