diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 0d3a156c7..3e42ecd08 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1335,6 +1335,10 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain
 }
 
 std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const {
+    if (term.size() == 0){
+        out << "0";
+        return out;
+    }
     bool first = true;
     for (const auto p : term) {
         mpq val = p.coeff();
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 5a30dc6dc..26bb8f64f 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -46,7 +46,7 @@ bool is_factor(const T & a, const T & b) {
             continue;
         } 
 
-        i++;
+        j++;
     }
 }
 
@@ -1074,7 +1074,12 @@ struct solver::imp {
                                               const rooted_mon& bd,
                                               const factor& b,
                                               const factor& d) {
-        
+        TRACE("nla_solver",
+              tout << "factor a = ";
+              print_factor(a, tout);
+              tout << ", factor b = ";
+              print_factor(b, tout););
+
         auto ac_m = vvr(a) * vvr(c);
         auto bd_m = vvr(b) * vvr(d);