From c5ff5ac2a13ae58eaedae6732e9902be7130ebb8 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 4 Jun 2018 12:33:36 -0700 Subject: [PATCH] Clen up spacer::pred_transformer::get_origin_summary --- src/muz/spacer/spacer_context.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index aaa379771..adcb8c8ae 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1142,7 +1142,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, expr_ref v(m); if (!must) { // use may summary - summary.push_back (get_formulas (level)); + summary.push_back (get_formulas(level)); // -- no auxiliary variables in lemmas *aux = nullptr; } else { // find must summary to use @@ -1160,10 +1160,10 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, } // -- pick an implicant - expr_ref_vector literals (m); - compute_implicant_literals (mev, summary, literals); + expr_ref_vector lits(m); + compute_implicant_literals (mev, summary, lits); - return mk_and(literals); + return mk_and(lits); }