mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 07:29:28 +00:00
Code Activity

stoi lemmas might have been forgotten so we need to reassert

Browse source
This commit is contained in:
CEisenhofer 2026-05-06 15:46:53 +02:00
parent 6fa354102a
commit e62ba9b60b
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_nseq.cpp
View file

@ -1594,11 +1594,15 @@ namespace smt {
ctx.mk_th_axiom(get_id(), 3, clause);
}
m_stoi_depth.insert_if_not_there(stoi_e, 0);
m_stoi_depth[stoi_e] = k;
if (m_stoi_depth.contains(stoi_e)) {
unsigned prev = m_stoi_depth[stoi_e];
ctx.push_trail(remove_obj_map(m_stoi_depth, stoi_e, prev));
m_stoi_depth.remove(stoi_e);
}
ctx.push_trail(insert_obj_map(m_stoi_depth, stoi_e));
m_stoi_depth.insert(stoi_e, k);
progress = true;
}
return !progress;
}