mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 22:57:51 +00:00
Code Activity

fix crash

Browse source
This commit is contained in:
Nuno Lopes 2026-02-10 10:33:36 +00:00
parent 915ad35012
commit bcca975d2d
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_consequences.cpp
View file

@ -60,7 +60,6 @@ namespace smt {
else { else {
justify(lit, s); justify(lit, s);
} }
m_antecedents.insert(lit.var(), std::move(s));
bool found = false; bool found = false;
if (m_var2val.contains(e)) { if (m_var2val.contains(e)) {
found = true; found = true;
@ -94,6 +93,7 @@ namespace smt {
fml = m.mk_implies(antecedent2fml(s), fml); fml = m.mk_implies(antecedent2fml(s), fml);
conseq.push_back(fml); conseq.push_back(fml);
} }
m_antecedents.insert(lit.var(), std::move(s));
} }
void context::justify(literal lit, index_set& s) { void context::justify(literal lit, index_set& s) {