mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Fix typo in comment

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 10:47:24 -07:00
parent 6514741e3f
commit 38a45f5482
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -636,7 +636,7 @@ class solve_eqs_tactic : public tactic {
TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";); TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
if (m_candidate_set.is_marked(f)) { if (m_candidate_set.is_marked(f)) {
// f may be deleted after the following update. // f may be deleted after the following update.
// so, we must remove remove the mark before doing the update // so, we must remove the mark before doing the update
m_candidate_set.mark(f, false); m_candidate_set.mark(f, false);
SASSERT(!m_candidate_set.is_marked(f)); SASSERT(!m_candidate_set.is_marked(f));
g.update(idx, m().mk_true(), m().mk_true_proof(), nullptr); g.update(idx, m().mk_true(), m().mk_true_proof(), nullptr);
@ -842,4 +842,3 @@ tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replace
else else
return clean(alloc(solve_eqs_tactic, m, p, r, false)); return clean(alloc(solve_eqs_tactic, m, p, r, false));
} }