From 1d9aad6ea9df35e939e34558b43a5a24eb823e19 Mon Sep 17 00:00:00 2001
From: Margus Veanes <veanes@users.noreply.github.com>
Date: Mon, 20 Dec 2021 17:44:06 -0800
Subject: [PATCH] improved regex merging avoiding unsat nontermination (#5728)

---
 src/ast/rewriter/seq_rewriter.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index aeda76da5..40a46ec0f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3331,7 +3331,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     SASSERT(m_util.is_re(r2));
     expr_ref result(m());
     std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
-    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); };
+    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); };
     if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1))
         result = r1;
     else if (re().is_empty(r1) || re().is_full_seq(r2))
@@ -3353,7 +3353,7 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
     if (re().is_epsilon(r2))
         std::swap(r1, r2);
     std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); };
-    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); };
+    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r1 : (is_subset(r2, r1) ? r2 : re().mk_inter(r1, r2))); };
     if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2))
         result = r1;
     else if (re().is_empty(r2) || re().is_full_seq(r1))
@@ -4598,6 +4598,8 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
             return true;
         if (re().is_full_seq(r2))
             return true;
+        if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
+            return true;
         if (is_concat(r1, ra1, ra2, ra3) &&
             is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
             r1 = ra3;