From bc3d8580c9bf0c28e7aa2b4b9eadac59480dd0bd Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Tue, 1 Aug 2017 10:12:29 +0200
Subject: [PATCH] fixed typo in optimized unsat core plugin code

---
 src/muz/spacer/spacer_unsat_core_plugin.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index 66abb32c6..5383fdc12 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -330,8 +330,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 {
                     SASSERT(!m_learner.is_a_marked(premise));
 
-                    // XXX AG: why is this condition is based on step and not on premise?
-                    if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(step)) && !m_learner.is_h_marked(step))
+                    if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(premise)) && !m_learner.is_h_marked(premise))
                     {
                         rational coefficient;
                         VERIFY(params[i].is_rational(coefficient));