change to iterative unfolding left build broken for some time

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · May 27, 2020 · 94ffd63 · 94ffd63
1 parent 9764007
commit 94ffd63
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 5 deletions.
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
@@ -250,7 +250,7 @@ class seq_util {
 #if Z3_USE_UNICODE
     bool is_char_le(expr const* e) const { return is_app_of(e, m_fid, OP_CHAR_LE); }
 #else
-    bool is_char_le(expr const* e) const { return false; }
+    bool is_char_le(expr const* e) const { return bv().is_bv_ule(e) && is_char(to_app(e)->get_arg(0)); }
 #endif
     app* mk_char(unsigned ch) const;
     app* mk_le(expr* ch1, expr* ch2) const;

diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
@@ -337,9 +337,9 @@ namespace smt {
                 continue;            
             lits.reset();
             lits.push_back(~lit);
-            if (!m.is_true(cond))
+            if (!m.is_true(cond)) 
                 lits.push_back(~th.mk_literal(cond));
-            if (false_literal != null_lit) 
+            if (null_lit != false_literal) 
                 lits.push_back(null_lit);
             if (!is_member(p.second, u))
                 lits.push_back(th.mk_literal(sk().mk_is_non_empty(p.second, re().mk_union(u, r))));
@@ -385,8 +385,13 @@ namespace smt {
             lits.reset();
             lits.push_back(~lit);
             expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
+            // TBD: triple check soundness here.
+            // elim_condition(x, x = 'a') = true
+            // forall x . x = 'a' => is_empty(r, u)
+            // <=> 
+            // is_empty(r, u)
             if (!m.is_true(cond)) {
-                lits.push_back(th.mk_literal(mk_forall(m, hd, m.mk_not(cond))));
+                lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
             }
             lits.push_back(th.mk_literal(is_empty1)); 
             th.add_axiom(lits);

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -3509,7 +3509,8 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
     if (k_min < UINT_MAX) {
         m_max_unfolding_depth++;
         k_min *= 2;
-        k_min = std::max(m_util.str.min_length(s_min), k_min);
+        if (m_util.is_seq(s_min))
+            k_min = std::max(m_util.str.min_length(s_min), k_min);
         IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");
         add_length_limit(s_min, k_min, false);
         return true;