mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

remove copy

Browse source
This commit is contained in:
Nuno Lopes 2020-07-14 12:26:49 +01:00
parent d1a0e83423
commit aeac0b46a0
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_ne_solver.cpp
View file

@ -224,10 +224,8 @@ bool theory_seq::reduce_ne(unsigned idx) {
TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n);); TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n););
if (updated) { if (updated) {
auto new_n(ne(n.l(), n.r(), new_eqs, new_lits, new_deps)); m_nqs.set(idx, ne(n.l(), n.r(), new_eqs, new_lits, new_deps));
m_nqs.set(idx, new_n);
TRACE("seq", display_disequation(tout << "updated:\n", m_nqs[idx]);); TRACE("seq", display_disequation(tout << "updated:\n", m_nqs[idx]););
TRACE("seq", display_disequation(tout << "updated:\n", new_n););
} }
return false; return false;
} }