From 088bd3ed8ecdf385f3ac8f0eb4fd05f844128c87 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 12 Oct 2017 12:40:42 -0400 Subject: [PATCH] Fix compiler warning --- src/muz/spacer/spacer_unsat_core_learner.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index 4adf67209..12b2a5614 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -155,7 +155,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e // check whether farkas lemma is to be interpolated (could potentially miss farkas lemmas, which are interpolated, because we potentially don't want to use the lowest cut) bool has_no_mixed_parents = true; - for (int i = 0; i < m.get_num_parents(currentNode); ++i) + for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) { proof* premise = to_app(currentNode->get_arg(i)); if (is_a_marked(premise) && is_b_marked(premise)) @@ -267,11 +267,11 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e verbose_stream() << "step"; } verbose_stream() << " from "; - for (int i = m.get_num_parents(currentNode) - 1; i >= 0 ; --i) + for (unsigned i = m.get_num_parents(currentNode); i > 0 ; --i) { proof* premise = to_app(currentNode->get_arg(i)); unsigned premise_small_id = id_to_small_id[premise->get_id()]; - if (i > 0) + if (i > 1) { verbose_stream() << premise_small_id << ", "; }