From e4f69bd78024ecaa0e08ad20a2b9d70c5432c465 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 May 2014 12:15:01 -0700 Subject: [PATCH] fix(kernel/justification): bug in depends_on Signed-off-by: Leonardo de Moura --- src/kernel/justification.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 93a8b9163..bf5b9c47a 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -137,8 +137,8 @@ bool depends_on(justification const & j, unsigned i) { return true; break; case justification_kind::Composite: case justification_kind::ExtComposite: - for (unsigned i = 0; i < 2; i++) { - justification c = to_composite(curr)->m_child[i]; + for (unsigned k = 0; k < 2; k++) { + justification c = to_composite(curr)->m_child[k]; if (may_contain(get_approx_assumption_set(c), i)) todo.push_back(c.raw()); }