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

Clen up spacer::pred_transformer::get_origin_summary

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-04 12:33:36 -07:00
parent d7dc10212e
commit c5ff5ac2a1
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/spacer/spacer_context.cpp
View file

@ -1142,7 +1142,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
expr_ref v(m); expr_ref v(m);
if (!must) { // use may summary if (!must) { // use may summary
summary.push_back (get_formulas (level)); summary.push_back (get_formulas(level));
// -- no auxiliary variables in lemmas // -- no auxiliary variables in lemmas
*aux = nullptr; *aux = nullptr;
} else { // find must summary to use } else { // find must summary to use
@ -1160,10 +1160,10 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
} }
// -- pick an implicant // -- pick an implicant
expr_ref_vector literals (m); expr_ref_vector lits(m);
compute_implicant_literals (mev, summary, literals); compute_implicant_literals (mev, summary, lits);
return mk_and(literals); return mk_and(lits);
} }