diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c056358a8..00e5b421b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2102,10 +2102,7 @@ public:
                 literal lit(ctx().get_bool_var(atom), pos);
                 core.push_back(~lit);
             }
-            std::cout << "the following conjunction should be unsat:\n";
-            ctx().display_literals_verbose(std::cout << "core ", core) << "\n";
-            display_evidence(std::cout, m_explanation); std::cout << "\n";
-            set_conflict(core);
+            set_conflict_or_lemma(core, false);
             break;
         }
         case l_true:
@@ -3174,10 +3171,10 @@ public:
 
     void set_conflict1() {
         literal_vector core;
-        set_conflict(core);
+        set_conflict_or_lemma(core, true);
     }
 
-    void set_conflict(literal_vector const& core) {
+    void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
         m_eqs.reset();
         m_core.reset();
         m_params.reset();
@@ -3185,12 +3182,6 @@ public:
             m_core.push_back(lit);
         }
         // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
-        /*
-          static unsigned cn = 0;
-          static unsigned num_l = 0;
-          num_l+=m_explanation.size();
-          std::cout << num_l / (++cn) << "\n";
-        */
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
         TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
@@ -3202,12 +3193,23 @@ public:
         }
         // SASSERT(validate_conflict());
         dump_conflict();
-        ctx().set_conflict(
-            ctx().mk_justification(
-                ext_theory_conflict_justification(
-                    get_id(), ctx().get_region(), 
-                    m_core.size(), m_core.c_ptr(), 
-                    m_eqs.size(), m_eqs.c_ptr(), m_params.size(), m_params.c_ptr())));
+        if (is_conflict) {
+            ctx().set_conflict(
+                ctx().mk_justification(
+                    ext_theory_conflict_justification(
+                        get_id(), ctx().get_region(), 
+                        m_core.size(), m_core.c_ptr(), 
+                        m_eqs.size(), m_eqs.c_ptr(), m_params.size(), m_params.c_ptr())));
+        }
+        else {
+            for (auto const& eq : m_eqs) {
+                m_core.push_back(th.mk_eq(eq.first->get_owner(), eq.second->get_owner(), false));
+            }
+            for (auto & c : m_core) {
+                c.neg();
+            }
+            ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
+        }
     }
 
     justification * why_is_diseq(theory_var v1, theory_var v2) {
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index e98cbf264..79a91e7e0 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -91,7 +91,7 @@ struct solver::imp {
         }
         
 
-        unsigned size() const { return m_map.size(); }
+        size_t size() const { return m_map.size(); }
         void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) {
             if (t->size() != 2 || ! t->m_v.is_zero())
                 return;
@@ -536,7 +536,7 @@ struct solver::imp {
     
     void get_large_and_small_indices_of_monomimal(const mon_eq& m,
                                                   vector<unsigned> & large,
-                                                  vector<unsigned> & small) {
+                                                  vector<unsigned> & _small) {
         
         for (unsigned i = 0; i < m.m_vs.size(); i++) {
             unsigned j = m.m_vs[i];
@@ -557,7 +557,7 @@ struct solver::imp {
             }
             
             if (is_set(lci) && is_set(uci) && -rational(1) <= lb && ub <= rational(1))
-                small.push_back(i);
+                _small.push_back(i);
         }
     }
 
@@ -683,8 +683,8 @@ struct solver::imp {
         std::cout << "generate_basic_lemma_for_mon_proportionality\n";
         const mon_eq & m = m_monomials[i_mon];
         vector<unsigned> large;
-        vector<unsigned> small;
-        get_large_and_small_indices_of_monomimal(m, large, small);
+        vector<unsigned> _small;
+        get_large_and_small_indices_of_monomimal(m, large, _small);
         
         // if abs(m.m_vs[j]) is 1, then ones_of_mon[j] = sign, where sign is 1 in case of m.m_vs[j] = 1, or -1 otherwise.
         if (m_minimal_monomials.empty())