diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h
index 7691554af..ed06d0825 100644
--- a/src/math/lp/explanation.h
+++ b/src/math/lp/explanation.h
@@ -18,47 +18,70 @@ Revision History:
 
 --*/
 #pragma once
-#include <unordered_set>
 #include "math/lp/lp_utils.h"
+#include "util/map.h"
+#include "util/optional.h"
 namespace lp {
 class explanation {
-    vector<std::pair<mpq, constraint_index>> m_explanation;
-    std::unordered_set<unsigned> m_set_of_ci;
+    u_map<optional<mpq>> m_j_to_mpq;   
 public:
     explanation() {}
     template <typename T>
-    explanation(const T& t) { for ( unsigned c : t) add(c); }
-    
-    void clear() { m_explanation.clear(); m_set_of_ci.clear(); }
-    vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
-    vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }
-    void push_justification(constraint_index j, const mpq& v) {
-        if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
-        m_set_of_ci.insert(j);
-        m_explanation.push_back(std::make_pair(v, j));
+    explanation(const T& t) {
+        for ( unsigned c : t)
+            push_back(c);
     }
-    void push_justification(constraint_index j) {
-        if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
-        m_set_of_ci.insert(j);
-        m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
+    
+    void clear() { m_j_to_mpq.reset(); }
+    void add_with_coeff(constraint_index j, const mpq& v) {
+        SASSERT(m_j_to_mpq.contains(j) == false); // if we hit the assert then we
+                                                  // might start using summation
+        m_j_to_mpq.insert(j, optional<mpq>(v));
     }
 
+    // this signature is needed to use it in a template that also works for the vector type
     void push_back(constraint_index j) {
-        push_justification(j);
+        if (m_j_to_mpq.contains(j))
+            return;
+        m_j_to_mpq.insert(j, optional<mpq>());
     }
     
-    void add(const explanation& e) {
-        for (const auto& p: e.m_explanation) {
-            add(p.second);
+    void add_expl(const explanation& e) {
+        for (const auto& p: e.m_j_to_mpq) {
+            m_j_to_mpq.insert(p.m_key, p.m_value);
         }
     }
-    template <typename T>
-    void add_expl(const T& e) { for (auto j: e) add(j); }
-    void add(unsigned ci) { push_justification(ci); }
-    
-    void add(const std::pair<mpq, constraint_index>& j) { push_justification(j.second, j.first); }
 
-    bool empty() const {  return m_explanation.empty();  }
-    size_t size() const { return m_explanation.size(); }
+    void add_pair(const std::pair<mpq, constraint_index>& j) {
+        add_with_coeff(j.second, j.first);
+    }
+
+    bool empty() const {  return m_j_to_mpq.empty();  }
+    size_t size() const { return m_j_to_mpq.size(); }
+
+    class cimpq {
+        constraint_index m_var;
+        const optional<mpq> & m_coeff;
+    public:
+        cimpq(constraint_index var, const optional<mpq> & val) : m_var(var), m_coeff(val) { }
+        constraint_index ci() const { return m_var; }
+        mpq coeff() const { return m_coeff.undef()? one_of_type<mpq>(): *m_coeff; }
+    };
+    class iterator {
+        u_map<optional<mpq>>::iterator m_it; 
+    public:
+        cimpq operator*() const {
+            return cimpq(m_it->m_key, m_it->m_value);
+        }        
+        iterator operator++() { iterator i = *this; m_it++; return i;  }
+        iterator operator++(int) { m_it++; return *this; }
+        iterator(u_map<optional<mpq>>::iterator it) : m_it(it) {}
+        bool operator==(const iterator &other) const { return m_it == other.m_it; }
+        bool operator!=(const iterator &other) const { return !(*this == other); }
+    };
+
+    iterator begin() const { return iterator(m_j_to_mpq.begin()); }
+    iterator end() const { return iterator(m_j_to_mpq.end()); }
+
 };
 }
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 14c908dbf..f2e496825 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -67,7 +67,7 @@ class create_cut {
             new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f);
             lp_assert(new_a.is_pos());
             m_k.addmul(new_a, lower_bound(j).x);
-            m_ex->push_justification(column_lower_bound_constraint(j));            
+            m_ex->push_back(column_lower_bound_constraint(j));            
         }
         else {
             lp_assert(at_upper(j));
@@ -75,7 +75,7 @@ class create_cut {
             new_a = - (m_fj <= m_f ? m_fj / m_f  : ((1 - m_fj) / m_one_minus_f));
             lp_assert(new_a.is_neg());
             m_k.addmul(new_a, upper_bound(j).x);
-            m_ex->push_justification(column_upper_bound_constraint(j));
+            m_ex->push_back(column_upper_bound_constraint(j));
         }
         m_t.add_monomial(new_a, j);
         m_lcm_den = lcm(m_lcm_den, denominator(new_a));
@@ -100,7 +100,7 @@ class create_cut {
             }
             m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
             // k += lower_bound(j).x * new_a;  
-            m_ex->push_justification(column_lower_bound_constraint(j));
+            m_ex->push_back(column_lower_bound_constraint(j));
         }
         else {
             lp_assert(at_upper(j));
@@ -113,7 +113,7 @@ class create_cut {
                 new_a =   a / m_one_minus_f; 
             }
             m_k.addmul(new_a, upper_bound(j).x); //  k += upper_bound(j).x * new_a; 
-            m_ex->push_justification(column_upper_bound_constraint(j));
+            m_ex->push_back(column_upper_bound_constraint(j));
         }
         m_t.add_monomial(new_a, j);
         TRACE("gomory_cut_detail_real", tout << "add " << new_a << "*v" << j << ", k: " << m_k << "\n";
@@ -320,8 +320,8 @@ public:
              // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T)
             try {
                 if (lia.is_fixed(j)) {
-                    m_ex->push_justification(column_lower_bound_constraint(j));
-                    m_ex->push_justification(column_upper_bound_constraint(j));
+                    m_ex->push_back(column_lower_bound_constraint(j));
+                    m_ex->push_back(column_upper_bound_constraint(j));
                     continue;
                 }
                 if (is_real(j)) {  
diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
index c7728474a..ad65a2b39 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -263,7 +263,7 @@ namespace lp  {
             lia.settings().stats().m_hnf_cuts++;
             lia.m_ex->clear();        
             for (unsigned i : constraints_for_explanation()) {
-                lia.m_ex->push_justification(i);
+                lia.m_ex->push_back(i);
             }
         } 
         return r;
diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h
index 19c5844ba..38e48f4aa 100644
--- a/src/math/lp/indexed_value.h
+++ b/src/math/lp/indexed_value.h
@@ -30,7 +30,7 @@ public:
     // for a column element it points to the row element offset
     unsigned m_other;
     indexed_value() {}
-    indexed_value(T v, unsigned i) : m_value(v), m_index(i) {}
+
     indexed_value(T v, unsigned i, unsigned other) :
         m_value(v), m_index(i), m_other(other) {
     }
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index 3976a0d3c..31c5274f9 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -51,7 +51,6 @@ lia_move int_branch::create_branch_on_column(int j) {
 }
 
 
-    
 int int_branch::find_inf_int_base_column() {
     int result = -1;
     mpq range;
@@ -59,7 +58,7 @@ int int_branch::find_inf_int_base_column() {
     mpq small_range_thresold(1024);
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-    unsigned prev_usage;
+    unsigned prev_usage = 0; // to quiet down the compile
     unsigned k = 0;
     unsigned usage;
     unsigned j;
@@ -103,5 +102,5 @@ int int_branch::find_inf_int_base_column() {
     }
     return result;    
 }
-    
+   
 }
diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp
index 53d13dbfe..f24cd47a0 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -210,8 +210,8 @@ namespace lp {
     void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
         constraint_index lc, uc;
         lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
-        lia.m_ex->push_justification(lc);
-        lia.m_ex->push_justification(uc);
+        lia.m_ex->push_back(lc);
+        lia.m_ex->push_back(uc);
     }
 
 }
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6f9c14bc7..f9f2e0696 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -307,8 +307,8 @@ void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evide
     
     // this is the case when the lower bound is in conflict with the upper one
     const ul_pair & ul =  m_columns_to_ul_pairs[m_crossed_bounds_column];
-    evidence.push_justification(ul.upper_bound_witness(),  numeric_traits<mpq>::one());
-    evidence.push_justification(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
+    evidence.add_with_coeff(ul.upper_bound_witness(),  numeric_traits<mpq>::one());
+    evidence.add_with_coeff(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
 }
 
     
@@ -1097,9 +1097,9 @@ bool lar_solver::inf_explanation_is_correct() const {
 
 mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
     mpq ret = numeric_traits<mpq>::zero();
-    for (auto & it : exp) {
-        mpq coeff = it.first;
-        constraint_index con_ind = it.second;
+    for (auto it : exp) {
+        mpq coeff = it.coeff();
+        constraint_index con_ind = it.ci();
         lp_assert(m_constraints.valid_index(con_ind));
         ret += (m_constraints[con_ind].rhs() - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
     }
@@ -1195,7 +1195,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
         constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
         lp_assert(m_constraints.valid_index(bound_constr_i));
-        exp.push_justification(bound_constr_i, coeff);
+        exp.add_with_coeff(bound_constr_i, coeff);
     } 
 }
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index fea075d27..66d2c7534 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -259,9 +259,9 @@ std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) con
 std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
     out << "expl: ";
     unsigned i = 0;
-    for (auto &p : exp) {
-        out << "(" << p.second << ")";
-        m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.second);
+    for (auto p : exp) {
+        out << "(" << p.ci() << ")";
+        m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.ci());
         if (++i < exp.size())
             out << "      ";
     }
@@ -312,7 +312,7 @@ bool core::explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& boun
         if (c + 1 == 0)
             return false;
         bound = a * m_lar_solver.get_lower_bound(p.column()).x;
-        e.add(c);
+        e.push_back(c);
         return true;
     }
     // a.is_neg()
@@ -320,7 +320,7 @@ bool core::explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& boun
     if (c + 1 == 0)
         return false;
     bound = a * m_lar_solver.get_upper_bound(p.column()).x;
-    e.add(c);
+    e.push_back(c);
     return true;
 }
 
@@ -334,7 +334,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun
         if (c + 1 == 0)
             return false;
         bound = a * m_lar_solver.get_lower_bound(j).x;
-        e.add(c);
+        e.push_back(c);
         return true;
     }
     // a.is_pos()
@@ -342,7 +342,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun
     if (c + 1 == 0)
         return false;
     bound = a * m_lar_solver.get_upper_bound(j).x;
-    e.add(c);
+    e.push_back(c);
     return true;
 }
     
@@ -855,7 +855,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
         }
     }
     for (const auto& p : l.expl()) {
-        const auto& c = m_lar_solver.constraints()[p.second];
+        const auto& c = m_lar_solver.constraints()[p.ci()];
         for (const auto& r : c.coeffs()) {
             insert_j(r.second);
         }
@@ -1060,7 +1060,7 @@ lemma& new_lemma::current() const {
 }
 
 new_lemma& new_lemma::operator&=(lp::explanation const& e) {
-    expl().add(e);
+    expl().add_expl(e);
     return *this;
 }
 
@@ -1124,7 +1124,7 @@ new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) {
 new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
     SASSERT(c.has_lower_bound(j));
     lp::explanation ex;
-    ex.add(c.m_lar_solver.get_column_lower_bound_witness(j));
+    ex.push_back(c.m_lar_solver.get_column_lower_bound_witness(j));
     *this &= ex;
     TRACE("nla_solver", tout << j << ": " << *this << "\n";);
     return *this;
@@ -1133,7 +1133,7 @@ new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
 new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
     SASSERT(c.has_upper_bound(j));
     lp::explanation ex;
-    ex.add(c.m_lar_solver.get_column_upper_bound_witness(j));
+    ex.push_back(c.m_lar_solver.get_column_upper_bound_witness(j));
     *this &= ex;
     return *this;
 }
@@ -1141,9 +1141,9 @@ new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
 std::ostream& new_lemma::display(std::ostream & out) const {
     auto const& lemma = current();
 
-    for (auto &p : lemma.expl()) {
-        out << "(" << p.second << ") ";
-        c.m_lar_solver.constraints().display(out, [this](lpvar j) { return c.var_str(j);}, p.second);
+    for (auto p : lemma.expl()) {
+        out << "(" << p.ci() << ") ";
+        c.m_lar_solver.constraints().display(out, [this](lpvar j) { return c.var_str(j);}, p.ci());
     }
     out << " ==> ";
     if (lemma.ineqs().empty()) {
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 2eb10801d..4ffbcb7e3 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -214,9 +214,9 @@ u_dependency *intervals::mk_dep(const lp::explanation& expl) {
     u_dependency * r = nullptr;
     for (auto p : expl) {
         if (r == nullptr) {
-            r = m_dep_intervals.mk_leaf(p.second);
+            r = m_dep_intervals.mk_leaf(p.ci());
         } else {
-            r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.second));
+            r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci()));
         }
     }
     return r;
@@ -285,7 +285,7 @@ bool intervals::interval_from_term(const nex& e, scoped_dep_interval& i) {
         m_dep_intervals.set_interval_for_scalar(i, b);
         if (wd == e_with_deps::with_deps) {
             for (auto p : exp) {
-                i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.second));
+                i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.ci()));
             }
             i.get().m_upper_dep = i.get().m_lower_dep;
         }
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index f7f2a7a94..047a5daff 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -94,7 +94,7 @@ struct solver::imp {
             m_nlsat->get_core(core);
             for (auto c : core) {
                 unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
-                ex.push_justification(idx, rational(1));
+                ex.push_back(idx);
                 TRACE("arith", tout << "ex: " << idx << "\n";);
             }
             nla::new_lemma lemma(m_nla_core, __FUNCTION__);
diff --git a/src/math/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h
index 3419ad5b7..df7f606fe 100644
--- a/src/math/lp/square_sparse_matrix_def.h
+++ b/src/math/lp/square_sparse_matrix_def.h
@@ -110,7 +110,7 @@ void square_sparse_matrix<T, X>::set_with_no_adjusting_for_row(unsigned row, uns
         }
     }
     // have not found the column between the indices
-    row_vec.push_back(indexed_value<T>(val, col)); // what about m_other ???
+    row_vec.push_back(indexed_value<T>(val, col, -1));
 }
 
 template <typename T, typename X>
@@ -123,7 +123,7 @@ void square_sparse_matrix<T, X>::set_with_no_adjusting_for_col(unsigned row, uns
         }
     }
     // have not found the column between the indices
-    col_vec.push_back(indexed_value<T>(val, row)); // what about m_other ???
+    col_vec.push_back(indexed_value<T>(val, row, -1)); 
 }
 
 
diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h
index 8da02e94e..24e90673d 100644
--- a/src/math/lp/var_eqs.h
+++ b/src/math/lp/var_eqs.h
@@ -43,7 +43,7 @@ public:
     void explain(lp::explanation& e) const {
         for (lpci c : m_cs)
             if (c + 1 != 0) // c != -1
-                e.add(c);
+                e.push_back(c);
     }
 };
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 573514d2e..26d7bb9fa 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2018,11 +2018,11 @@ public:
             }
         }
         for (auto const& ev : ex) {
-            lp().constraints().display(out << ev.first << ": ", ev.second);
+            lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
         }
         expr_ref_vector fmls(m);
         for (auto const& ev : ex) {
-            fmls.push_back(constraint2fml(ev.second));
+            fmls.push_back(constraint2fml(ev.ci()));
         }        
         expr_ref t(term2expr(term), m);
         if (upper) {
@@ -2081,9 +2081,7 @@ public:
             // m_explanation implies term <= k
             reset_evidence();
             for (auto const& ev : m_explanation) {
-                if (!ev.first.is_zero()) { 
-                    set_evidence(ev.second, m_core, m_eqs);
-                }
+                set_evidence(ev.ci(), m_core, m_eqs);
             }
             // The call mk_bound() can set the m_infeasible_column in lar_solver
             // so the explanation is safer to take before this call.
@@ -2335,7 +2333,7 @@ public:
 
         void consume(rational const& v, lp::constraint_index j) override {
             m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs);
-            m_imp.m_explanation.push_justification(j, v);
+            m_imp.m_explanation.add_with_coeff(j, v);
         }
     };
 
@@ -3273,9 +3271,7 @@ public:
         TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
         TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto const& ev : m_explanation) {
-            if (!ev.first.is_zero()) { 
-                set_evidence(ev.second, m_core, m_eqs);
-            }
+            set_evidence(ev.ci(), m_core, m_eqs);
         }
         // SASSERT(validate_conflict(m_core, m_eqs));
         dump_conflict(m_core, m_eqs);
@@ -3785,11 +3781,11 @@ public:
     void display_evidence(std::ostream& out, lp::explanation const& evidence) {
         for (auto const& ev : evidence) {
             expr_ref e(m);
-            SASSERT(!ev.first.is_zero()); 
-            if (ev.first.is_zero()) { 
+            SASSERT(!ev.coeff().is_zero()); 
+            if (ev.coeff().is_zero()) { 
                 continue;
             }
-            unsigned idx = ev.second;
+            unsigned idx = ev.ci();
             switch (m_constraint_sources.get(idx, null_source)) {
             case inequality_source: {
                 literal lit = m_inequalities[idx];
@@ -3816,7 +3812,7 @@ public:
             }
         }
         for (auto const& ev : evidence) {
-            lp().constraints().display(out << ev.first << ": ", ev.second); 
+            lp().constraints().display(out << ev.coeff() << ": ", ev.ci()); 
         }
     }
 
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index 16d33794e..4c2d68c5f 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -67,7 +67,7 @@ struct gomory_test {
             }
             k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than
             // k += lower_bound(x_j).x * new_a;  
-            expl.push_justification(column_lower_bound_constraint(x_j), new_a);
+            expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a);
         }
         else {
             lp_assert(at_upper(x_j));
@@ -79,7 +79,7 @@ struct gomory_test {
                 new_a =   a / (mpq(1) - f_0); 
             }
             k.addmul(new_a, upper_bound(x_j).x); //  k += upper_bound(x_j).x * new_a; 
-            expl.push_justification(column_upper_bound_constraint(x_j), new_a);
+            expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a);
         }
         TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << k << "\n";);
         pol.add_monomial(new_a, x_j);
@@ -107,7 +107,7 @@ struct gomory_test {
                 new_a = (1 - f_j) / f_0;
             }
             k.addmul(new_a, lower_bound(x_j).x);
-            expl.push_justification(column_lower_bound_constraint(x_j), new_a);
+            expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a);
         }
         else {
             lp_assert(at_upper(x_j));
@@ -119,7 +119,7 @@ struct gomory_test {
             }
             new_a.neg(); // the upper terms are inverted
             k.addmul(new_a, upper_bound(x_j).x);
-            expl.push_justification(column_upper_bound_constraint(x_j), new_a);
+            expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a);
         }
         TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << k << "\n";);
         t.add_monomial(new_a, x_j);
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index e40232a81..ae843d59b 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -78,6 +78,7 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
 }
 
 void test_nex_order() {
+#if Z3DEBUG
     enable_trace("nla_cn");
     enable_trace("nla_cn_details");
     // enable_trace("nla_cn_details_");
@@ -116,6 +117,7 @@ void test_nex_order() {
     nex_mul * poly = r.mk_mul(five_a_pl_one, b);
     nex * p = r.simplify(poly);
     std::cout << "poly = " << *poly << " , p = " << *p << "\n";
+#endif
 }
 
 void test_simplify() {
diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp
index f52f303ce..6e2e0336a 100644
--- a/src/test/lp/nla_solver_test.cpp
+++ b/src/test/lp/nla_solver_test.cpp
@@ -218,7 +218,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
         } 
     }
 
-    SASSERT(found0 && (found1 || found2));
+    VERIFY(found0 && (found1 || found2));
 
     
 }
@@ -289,7 +289,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
 
     }
 
-    SASSERT(found0 && found1 && found2 && found3);
+    VERIFY(found0 && found1 && found2 && found3);
 
 }
 void test_basic_lemma_for_mon_neutral_from_factors_to_monomial() {
@@ -364,7 +364,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
         }
     }
 
-    SASSERT(found0 && found1);
+    VERIFY(found0 && found1);
 }
 
 void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
@@ -416,7 +416,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
         }
     }
 
-    SASSERT(found0 && found1 && found2);
+    VERIFY(found0 && found1 && found2);
     
 }
 
@@ -488,7 +488,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
         }
     }
 
-    SASSERT(found0 && found1);
+    VERIFY(found0 && found1);
 }
 
 void test_horner() {