mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
74890ca1c8
commit
62b8394bdd
|
@ -181,6 +181,7 @@ namespace smt {
|
|||
enode * m_node2;
|
||||
public:
|
||||
eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
|
||||
SASSERT(n1 != n2);
|
||||
}
|
||||
|
||||
virtual void get_antecedents(conflict_resolution & cr);
|
||||
|
|
|
@ -1891,7 +1891,7 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
new_ls.push_back(ls);
|
||||
new_rs.push_back(rs);
|
||||
}
|
||||
else {
|
||||
else if (nl != nr) {
|
||||
literal lit(mk_eq(nl, nr, false));
|
||||
ctx.mark_as_relevant(lit);
|
||||
new_lits.push_back(lit);
|
||||
|
|
Loading…
Reference in a new issue