From 6a90072a983808edb7d935ef287cd722cba2a306 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 May 2020 12:03:40 -0700
Subject: [PATCH] bug in non-member disjunction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp           | 5 +----
 src/ast/rewriter/seq_rewriter.cpp | 2 +-
 src/smt/seq_regex.cpp             | 4 +++-
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 0c818b848..f040bf47e 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -816,10 +816,7 @@ class smt2_printer {
         TRACE("pp_let", tout << "decls.size(): " << decls.size() << "\n";);
         ptr_buffer<format> buf;
         unsigned num_op = 0;
-        vector<ptr_vector<format> >::iterator it  = decls.begin();
-        vector<ptr_vector<format> >::iterator end = decls.end();
-        for (; it != end; ++it) {
-            ptr_vector<format> & lvl_decls = *it;
+        for (ptr_vector<format> & lvl_decls : decls) {
             if (lvl_decls.empty())
                 continue;
             if (num_op > 0)
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 703512115..0927f7b26 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2717,7 +2717,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
             else {
                 ranges1.reset();
                 ranges1.append(ranges);
-                intersect(0, ch-1, ranges);
+                intersect(0, ch - 1, ranges);
                 intersect(ch + 1, zstring::max_char(), ranges1);
                 ranges.append(ranges1);
             }
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 6ba2b5130..df9ff2bcc 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -303,7 +303,7 @@ namespace smt {
     }
 
     /**
-     * is_non_empty(r, u) => nullable or not c_i or is_non_empty(r_i, u union r)
+     * is_non_empty(r, u) => nullable or \/_i (c_i and is_non_empty(r_i, u union r))
      *
      * for each (c_i, r_i) in cofactors (min-terms)
      *
@@ -337,6 +337,8 @@ namespace smt {
             if (m.is_false(cond))
                 continue;            
             expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
+            if (!m.is_true(cond))
+                next_non_empty = m.mk_and(cond, next_non_empty);
             lits.push_back(th.mk_literal(next_non_empty));
         }
         th.add_axiom(lits);