mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #2018

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-12-05 00:54:10 -08:00
parent dc77579707
commit 9635ddd8fc
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -4561,11 +4561,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
IF_VERBOSE(11, verbose_stream() << "intersect " << re << " " << mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";); IF_VERBOSE(11, verbose_stream() << "intersect " << re << " " << mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";);
re = m_util.re.mk_inter(entry.m_re, re); re = m_util.re.mk_inter(entry.m_re, re);
m_rewrite(re); m_rewrite(re);
lits.push_back(entry.m_lit); lits.push_back(~entry.m_lit);
enode* n1 = ensure_enode(entry.m_s); enode* n1 = ensure_enode(entry.m_s);
enode* n2 = ensure_enode(s); enode* n2 = ensure_enode(s);
if (n1 != n2) { if (n1 != n2) {
lits.push_back(mk_eq(n1->get_owner(), n2->get_owner(), false)); lits.push_back(~mk_eq(n1->get_owner(), n2->get_owner(), false));
} }
} }
} }