diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index daeb09b8a..a4d32b505 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -85,8 +85,10 @@ namespace qe {
             if (m_flevel.find(a->get_decl(), lvl)) {
                 lvl0.merge(lvl);
             }
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                app* arg = to_app(a->get_arg(i));
+            for (expr* f : *a) {
+                if (!is_app(f))
+                    throw tactic_exception("atom is non-ground");
+                app* arg = to_app(f);
                 if (m_elevel.find(arg, lvl)) {
                     lvl0.merge(lvl);
                 }
@@ -265,12 +267,9 @@ namespace qe {
                 continue;
             }
             
-            unsigned sz = a->get_num_args();
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* f = a->get_arg(i);
-                if (!mark.is_marked(f)) {
-                    todo.push_back(f);
-                }
+            for (expr* f : *a) {
+                if (!mark.is_marked(f))
+                    todo.push_back(f);                
             } 
             
             bool is_boolop = 
@@ -324,8 +323,8 @@ namespace qe {
             unsigned sz = a->get_num_args();
             bool diff = false;
             args.reset();
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* f = a->get_arg(i), *f1;
+            for (expr* f : *a) {
+                expr *f1;
                 if (cache.find(f, f1)) {
                     args.push_back(f1);
                     diff |= f != f1;
@@ -413,8 +412,8 @@ namespace qe {
             unsigned sz = a->get_num_args();
             args.reset();
             bool diff = false;
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* f = a->get_arg(i), *f1;
+            for (expr* f : *a) {
+                expr *f1;
                 if (cache.find(f, f1)) {
                     args.push_back(f1);
                     diff |= f != f1;
@@ -1018,12 +1017,12 @@ namespace qe {
                     expr_ref_vector args(m);
                     unsigned num_args = a->get_num_args();
                     bool all_visited = true;
-                    for (unsigned i = 0; i < num_args; ++i) {
-                        if (visited.find(a->get_arg(i), r)) {
+                    for (expr* arg : *a) {
+                        if (visited.find(arg, r)) {
                             args.push_back(r);
                         }
                         else {
-                            todo.push_back(a->get_arg(i));
+                            todo.push_back(arg);
                             all_visited = false;
                         }
                     }