From d21911c0732630b4196037ba03f80bb0a3986e33 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 24 Apr 2020 17:49:26 -0500
Subject: [PATCH] z3str3: fix support for re.complement and re.intersection

---
 src/smt/theory_str.cpp       | 12 ++++++++++++
 src/smt/theory_str_regex.cpp |  6 +++++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 98e36a6a948..9a346c50747 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2069,6 +2069,18 @@ namespace smt {
             return zstring("(.*)");
         } else if (u.re.is_full_char(a_regex)) {
             return zstring("str.allchar");
+        } else if (u.re.is_intersection(a_regex)) {
+            expr * a0;
+            expr * a1;
+            u.re.is_intersection(a_regex, a0, a1);
+            zstring a0str = get_std_regex_str(a0);
+            zstring a1str = get_std_regex_str(a1);
+            return zstring("(") + a0str + zstring("&&") + a1str + zstring(")");
+        } else if (u.re.is_complement(a_regex)) {
+            expr * body;
+            u.re.is_complement(a_regex, body);
+            zstring bodyStr = get_std_regex_str(body);
+            return zstring("(^") + bodyStr + zstring(")");
         } else {
             TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
             UNREACHABLE(); return zstring("");
diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
index 0f6b7e4cb45..0b5d831fc45 100644
--- a/src/smt/theory_str_regex.cpp
+++ b/src/smt/theory_str_regex.cpp
@@ -902,7 +902,11 @@ namespace smt {
             return true;
         } else if (u.re.is_complement(re)) {
             // TODO can we do better?
-                    return false;
+            return false;
+        } else if (u.re.is_intersection(re)) {
+            return false;
+        } else if (u.re.is_complement(re)) {
+            return false;
         } else if (u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
             return check_regex_length_linearity_helper(sub1, already_star);
         } else {