diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp
index 08f7f7ce8..730ef1629 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.cpp
+++ b/src/muz/spacer/spacer_unsat_core_learner.cpp
@@ -54,7 +54,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
         // if the node mixes A-reasoning and B-reasoning
         // and contains non-closed premises
         if (!done) {
-            if (m_pr.is_a_marked(curr) && m_pr.is_b_marked(curr)) {
+            if (is_a(curr) && is_b(curr)) {
                 compute_partial_core(curr);
             }
         }
@@ -92,9 +92,6 @@ void unsat_core_learner::set_closed(proof* p, bool value) {
     m_closed.mark(p, value);
 }
 
-bool unsat_core_learner::is_b_open(proof *p) {
-    return m_pr.is_b_marked(p) && !is_closed (p);
-}
 
 void unsat_core_learner::add_lemma_to_core(expr* lemma) {
     m_unsat_core.push_back(lemma);
diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h
index 42ad71501..ead430ca0 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.h
+++ b/src/muz/spacer/spacer_unsat_core_learner.h
@@ -47,10 +47,17 @@ namespace spacer {
 
         ast_manager& get_manager() {return m;}
 
-        bool is_a(proof *pr) {return m_pr.is_a_marked(pr);}
+
+        bool is_a(proof *pr) {
+            // AG: treat hypotheses as A
+            // AG: assume that all B-hyp have been eliminated
+            // AG: this is not yet true in case of arithmetic eq_prop
+            return m_pr.is_a_marked(pr) || is_h(pr);
+        }
         bool is_b(proof *pr) {return m_pr.is_b_marked(pr);}
         bool is_h(proof *pr) {return m_pr.is_h_marked(pr);}
         bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);}
+        bool is_b_open(proof *p) {return m_pr.is_b_marked(p) && !is_closed (p);}
 
         /*
          * register a plugin for computation of partial unsat cores
@@ -72,7 +79,6 @@ namespace spacer {
         bool is_closed(proof* p);
         void set_closed(proof* p, bool value);
 
-        bool is_b_open (proof *p);
 
         /*
          * adds a lemma to the unsat core
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index ef97d81df..aeb509c2e 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -210,6 +210,7 @@ namespace spacer {
             // AG: it will go into the core. However, it does not mean that this literal should/could not be added.
             m_ctx.set_closed(step, done);
             expr_ref res = compute_linear_combination(coeff_lits);
+            TRACE("spacer.farkas", tout << "Farkas core: " << res << "\n";);
             m_ctx.add_lemma_to_core(res);
         }
     }