diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 2a46fd07f..fb67d91d6 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -426,6 +426,7 @@ namespace smt {
         std::stringstream strm;
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
         std::ofstream out(strm.str());
+        TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
         out.close();
         return m_lemma_id;
@@ -466,6 +467,7 @@ namespace smt {
         std::stringstream strm;
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
         std::ofstream out(strm.str());
+        TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
         return m_lemma_id;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d079f31ed..a67fead38 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1512,7 +1512,7 @@ public:
             if (r1.is_int() && r2.is_int() && r == div(r1, r2)) {
                 continue;
             }
-            if (r2.is_neg()) {
+            if (r2.is_neg() || r1.is_neg()) {
                 // TBD
                 continue;
             }
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index 094b27ed3..4ae93a52e 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -217,13 +217,12 @@ struct mus::imp {
         }
 
         expr_set mss_set;
-        for (unsigned i = 0; i < mss.size(); ++i) {
-            mss_set.insert(mss[i]);
+        for (expr* e : mss) {
+            mss_set.insert(e);
         }
-        expr_set::iterator it = min_core.begin(), end = min_core.end();
-        for (; it != end; ++it) {
-            if (mss_set.contains(*it) && min_lit != *it) {
-                unknown.push_back(*it);
+        for (expr * e : min_core) {
+            if (mss_set.contains(e) && min_lit != e) {
+                unknown.push_back(e);
             }
         }
         core_literal = min_lit;