diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 974550b42..b40c11c58 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -433,7 +433,7 @@ namespace qe {
             s.m_solver.vars(l, vs);
             TRACE("qe", s.m_solver.display(tout << vs << " ", l) << "\n";);
             for (unsigned v : vs) {
-                level.merge(s.m_rvar2level[v]);                
+                level.merge(s.m_rvar2level.get(v, max_level()));                
             }
             set_level(l.var(), level);
             return level;
diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index 1d87953ab..fe31aa50a 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -140,7 +140,6 @@ namespace sat {
             r |= ((n.lut() >> w) & 0x1) << j;
         } 
         a.set_table(r);
-        std::cout << a << "\n";
         insert_cut(v, a, cs);
     }
 
@@ -149,6 +148,9 @@ namespace sat {
         literal l1 = child(n, 0);
         literal l2 = child(n, 1);
         literal l3 = child(n, 2);
+        VERIFY(&cs != &m_cuts[l1.var()]);
+        VERIFY(&cs != &m_cuts[l2.var()]);
+        VERIFY(&cs != &m_cuts[l3.var()]);
         for (auto const& a : m_cuts[l1.var()]) {
             for (auto const& b : m_cuts[l2.var()]) {
                 cut ab;
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 50d606197..1a583dac6 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -418,8 +418,7 @@ private:
     }
 
     bool pure_args(app* a) const {
-        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            expr* e = a->get_arg(i);
+        for (expr* e : *a) { 
             m.is_not(e, e);
             if (!is_uninterp_const(e) && !m.is_true(e) && !m.is_false(e)) {
                 return false;
@@ -566,7 +565,8 @@ private:
         }
         else if (pb.is_ge(e)) {
             app* a = to_app(e);
-            SASSERT(pure_args(a));
+            if (!pure_args(a))
+                return false;
             for (unsigned i = 0; i < a->get_num_args(); ++i) {
                 args.push_back(a->get_arg(i));
                 coeffs.push_back(pb.get_coeff(a, i));
@@ -575,9 +575,10 @@ private:
         }
         else if (m.is_or(e)) {
             app* a = to_app(e);
-            SASSERT(pure_args(a));
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                args.push_back(a->get_arg(i));
+            if (!pure_args(a))
+                return false; 
+            for (expr* arg : *a) {
+                args.push_back(arg);
                 coeffs.push_back(rational::one());
             }
             k = rational::one();