better behavior on disequality and branch selection

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jul 31, 2020 · 4392c03 · 4392c03
1 parent 02084dc
commit 4392c03
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -3101,7 +3101,12 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
         }
 
         dependency* dep = m_dm.mk_leaf(assumption(~lit));
-        m_nqs.push_back(ne(e1, e2, dep));
+        expr_ref len1(m_util.str.mk_length(e1), m);
+        expr_ref len2(m_util.str.mk_length(e2), m);
+        m_rewrite(len1);
+        m_rewrite(len2);
+        literal eqlen = mk_eq(len1, len2, false); 
+        m_nqs.push_back(ne(e1, e2, eqlen, dep));
         if (ctx.get_assignment(lit) != l_undef) {
             solve_nqs(m_nqs.size() - 1);
         }

diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
@@ -178,11 +178,12 @@ namespace smt {
             literal_vector           m_lits;
             dependency*              m_dep;
         public:
-            ne(expr_ref const& l, expr_ref const& r, dependency* dep):
+            ne(expr_ref const& l, expr_ref const& r, literal eqlen, dependency* dep):
                 m_l(l), m_r(r), m_dep(dep) {
                     expr_ref_vector ls(l.get_manager()); ls.push_back(l);
                     expr_ref_vector rs(r.get_manager()); rs.push_back(r);
                     m_eqs.push_back(std::make_pair(ls, rs));
+                    m_lits.push_back(eqlen);
                 }
 
             ne(expr_ref const& _l, expr_ref const& _r, vector<decomposed_eq> const& eqs, literal_vector const& lits, dependency* dep):