diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 9435a49cd..e7037f31a 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -260,7 +260,7 @@ namespace smt {
             bool is_atom() const { return m_atom; }
             inf_numeral const & get_value() const { return m_value; }
             virtual bool has_justification() const { return false; }
-            virtual void push_justification(antecedents& antecedents, numeral const& coeff) {}
+            virtual void push_justification(antecedents& antecedents, numeral const& coeff, bool proofs_enabled) {}
         };
 
 
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 1e15365a4..9f77934e5 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -749,7 +749,7 @@ namespace smt {
     void theory_arith<Ext>::accumulate_justification(bound & b, derived_bound& new_bound, numeral const& coeff, literal_idx_set & lits, eq_set & eqs) {
         antecedents& ante = m_tmp_antecedents;
         ante.reset();
-        b.push_justification(ante, coeff);
+        b.push_justification(ante, coeff, proofs_enabled());
         unsigned num_lits = ante.lits().size();
         for (unsigned i = 0; i < num_lits; ++i) {
             literal l = ante.lits()[i];
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 0f3ed1d13..b774fb3d9 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1979,7 +1979,7 @@ namespace smt {
               tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";);
         antecedents& ante = get_antecedents();
         explain_bound(r, idx, !is_below, delta, ante);
-        b->push_justification(ante, numeral(1));
+        b->push_justification(ante, numeral(1), proofs_enabled());
        
 
         set_conflict(ante.lits().size(), ante.lits().c_ptr(), 
@@ -2122,8 +2122,8 @@ namespace smt {
     void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) {
         SASSERT(b1->get_var() == b2->get_var());
         antecedents& ante = get_antecedents();
-        b1->push_justification(ante, numeral(1));
-        b2->push_justification(ante, numeral(1));
+        b1->push_justification(ante, numeral(1), proofs_enabled());
+        b2->push_justification(ante, numeral(1), proofs_enabled());
 
         set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
         TRACE("arith_conflict", tout << "bound conflict\n";);
@@ -2382,7 +2382,7 @@ namespace smt {
                 if (!b->has_justification())
                     continue;
                 if (!relax_bounds() || delta.is_zero()) {
-                    b->push_justification(ante, it->m_coeff);
+                    b->push_justification(ante, it->m_coeff, proofs_enabled());
                     continue;
                 }
                 numeral coeff = it->m_coeff;
@@ -2442,7 +2442,7 @@ namespace smt {
                 SASSERT(!is_b_lower || k_2 <= k_1);
                 SASSERT(is_b_lower  || k_2 >= k_1);
                 if (new_atom == 0) {
-                    b->push_justification(ante, coeff);
+                    b->push_justification(ante, coeff, proofs_enabled());
                     continue;
                 }
                 SASSERT(!is_b_lower || k_2 < k_1);
@@ -2686,8 +2686,8 @@ namespace smt {
         typename vector<row_entry>::const_iterator end = r.end_entries();
         for (; it != end; ++it) {
             if (!it->is_dead() && is_fixed(it->m_var)) {
-                lower(it->m_var)->push_justification(antecedents, it->m_coeff);
-                upper(it->m_var)->push_justification(antecedents, it->m_coeff);                
+                lower(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());
+                upper(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());                
             }
         }
     }
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index e6130acfe..04e16e778 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -59,10 +59,10 @@ namespace smt {
                     // v >= k >= v2 => v >= v2
                     // 
 
-                    lower(v)->push_justification(ante, numeral::zero());
-                    upper(v2)->push_justification(ante, numeral::zero());
-                    lower(v2)->push_justification(ante, numeral::zero());
-                    upper(v)->push_justification(ante, numeral::zero());
+                    lower(v)->push_justification(ante, numeral::zero(), proofs_enabled());
+                    upper(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
+                    lower(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
+                    upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
 
                     TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
                           display_var(tout, v);
@@ -247,8 +247,8 @@ namespace smt {
                     //
                     // x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2
                     // 
-                    lower(x2)->push_justification(ante, numeral::zero());
-                    upper(x2)->push_justification(ante, numeral::zero());
+                    lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
+                    upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     m_stats.m_fixed_eqs++;
                     propagate_eq_to_core(x, x2, ante);
                 }
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 2a3bff804..e0ecc087a 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -525,7 +525,7 @@ namespace smt {
                         }
                         // k += new_a_ij * lower_bound(x_j).get_rational();
                         k.addmul(new_a_ij, lower_bound(x_j).get_rational());
-                        lower(x_j)->push_justification(ante, numeral::zero());
+                        lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
                     }
                     else {
                         SASSERT(at_upper(x_j));
@@ -541,7 +541,7 @@ namespace smt {
                         }
                         // k += new_a_ij * upper_bound(x_j).get_rational();
                         k.addmul(new_a_ij, upper_bound(x_j).get_rational());
-                        upper(x_j)->push_justification(ante, numeral::zero());
+                        upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
                     }
                     pol.push_back(row_entry(new_a_ij, x_j));
                 }
@@ -566,7 +566,7 @@ namespace smt {
                             }
                             // k += new_a_ij * lower_bound(x_j).get_rational();
                             k.addmul(new_a_ij, lower_bound(x_j).get_rational());
-                            lower(x_j)->push_justification(ante, numeral::zero());
+                            lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
                         }
                         else {
                             SASSERT(at_upper(x_j));
@@ -579,7 +579,7 @@ namespace smt {
                             new_a_ij.neg(); // the upper terms are inverted
                             // k += new_a_ij * upper_bound(x_j).get_rational();
                             k.addmul(new_a_ij, upper_bound(x_j).get_rational());
-                            upper(x_j)->push_justification(ante, numeral::zero());
+                            upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
                         }
                         TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
                         pol.push_back(row_entry(new_a_ij, x_j));
@@ -772,8 +772,8 @@ namespace smt {
                         // u += ncoeff * lower_bound(v).get_rational();
                         u.addmul(ncoeff, lower_bound(v).get_rational());
                     }
-                    lower(v)->push_justification(ante, numeral::zero());
-                    upper(v)->push_justification(ante, numeral::zero());
+                    lower(v)->push_justification(ante, numeral::zero(), proofs_enabled());
+                    upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
                 }
                 else if (gcds.is_zero()) {
                     gcds = abs_ncoeff;