diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 65690f7eb..fd36d391c 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -357,25 +357,35 @@ void asserted_formulas::flatten_clauses() {
     if (m.proofs_enabled()) return;
     bool change = true;
     vector<justified_expr> new_fmls;
+    auto mk_not = [this](expr* e) { return m.is_not(e, e) ? e : m.mk_not(e); };
+    auto is_literal = [this](expr *e) { m.is_not(e, e); return !is_app(e) || to_app(e)->get_num_args() == 0; };
+    expr *a = nullptr, *b = nullptr, *c = nullptr;
     while (change) {
         change = false;        
         new_fmls.reset();
         unsigned sz = m_formulas.size();
         for (unsigned i = m_qhead; i < sz; ++i) {
             auto const& j = m_formulas.get(i);
-            expr* f = j.get_fml(), *a = nullptr, *b = nullptr;
+            expr* f = j.get_fml();
             bool decomposed = false;
-            if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && b->get_ref_count() == 1) {
+            if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
                 decomposed = true;
             }
-            else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && b->get_ref_count() == 1) {
+            else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
                 decomposed = true;
-            }
+            }            
             if (decomposed) {
                 for (expr* arg : *to_app(b)) {
-                    justified_expr j1(m, m.mk_or(a, m.is_not(arg, arg) ? arg : m.mk_not(arg)), nullptr);
+                    justified_expr j1(m, m.mk_or(a, mk_not(arg)), nullptr);
                     new_fmls.push_back(j1);
                 }
+                change = true;
+                continue;
+            }
+            if (m.is_ite(f, a, b, c)) {
+                new_fmls.push_back(justified_expr(m, m.mk_or(mk_not(a), b), nullptr));
+                new_fmls.push_back(justified_expr(m, m.mk_or(a, c), nullptr));
+                change = true;
                 continue;
             }
             new_fmls.push_back(j);            
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 8413d06e5..d56ba30ea 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -34,7 +34,7 @@ namespace smt {
         SASSERT(is_watching_clause(~cls->get_literal(1), cls));        
         for (literal l : *cls) {
             // holds, TBD re-enable when ready to re-check
-            // SASSERT(m_lit_occs[l.index()] > 0);
+            // SASSERT(!track_occs() || m_lit_occs[l.index()] > 0);
         }
         return true;
     }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index dfdcc61fc..3ebca8673 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1922,7 +1922,6 @@ public:
             theory_var v1 = mk_var(p);
             lp::impq r1 = get_ivalue(v1);
             SASSERT(r1.y.is_zero());
-            SASSERT(r1.x.is_int());
             rational r2;
 
             if (!r1.x.is_int() || r1.x.is_neg()) {
@@ -1942,7 +1941,6 @@ public:
                 }
                 lp::impq val_v = get_ivalue(v);
                 SASSERT(val_v.y.is_zero());
-                SASSERT(val_v.x.is_int());
                 if (val_v.x == div(r1.x, r2)) continue;
             
                 TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);