diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 3b6dea6f5..d4b93b90c 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -149,7 +149,7 @@ namespace sat {
             for (literal lit : m_solver.get_core())
                 m_core.push_back(lit2ext(lit));        
         if (is_sat == l_true) {
-            TRACE("dual", display(s, tout); s.display(tout););
+            TRACE("dual", display(tout); s.display(tout););
             IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
             IF_VERBOSE(0, verbose_stream() << "assumptions: " << m_lits << "\n");
             IF_VERBOSE(0, display(verbose_stream()); s.display(verbose_stream()););
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 6d20072cb..9ad2a17ed 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -378,9 +378,7 @@ namespace smt {
                 break;
             case l_true: {
                 expr * true_arg = nullptr;
-                unsigned num_args = n->get_num_args();
-                for (unsigned i = 0; i < num_args; i++) {
-                    expr * arg  = n->get_arg(i);
+                for (expr* arg : *n) {
                     if (m_context.find_assignment(arg) == l_true) {
                         if (is_relevant_core(arg))
                             return;
@@ -402,9 +400,7 @@ namespace smt {
             switch (val) {
             case l_false: {
                 expr * false_arg = nullptr;
-                unsigned num_args = n->get_num_args();
-                for (unsigned i = 0; i < num_args; i++) {
-                    expr * arg  = n->get_arg(i);
+                for (expr* arg : *n) {
                     if (m_context.find_assignment(arg) == l_false) {
                         if (is_relevant_core(arg))
                             return;