diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index 43fe047c2..4d506f2bb 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -266,7 +266,7 @@ namespace sls {
         a.m_last_delta = delta;
         a.m_last_var = v;
         TRACE("arith", tout << mt << " v" << v << " " << mk_bounded_pp(a.m_vars[v].m_expr, a.m) 
-                            << " += " << delta << " score:" << a.m_best_score << "\n");
+                            << " += " << delta << " score:" << m_best_score << "\n");
         a.m_vars[v].set_step(a.m_stats.m_steps, a.m_stats.m_steps + 3 + ctx.rand(10), delta);
         VERIFY(a.update_num(v, delta));
         for (auto bv : a.m_vars[v].m_bool_vars_of) 
diff --git a/src/ast/sls/sls_arith_lookahead.cpp b/src/ast/sls/sls_arith_lookahead.cpp
index 7c665390f..1db76cf36 100644
--- a/src/ast/sls/sls_arith_lookahead.cpp
+++ b/src/ast/sls/sls_arith_lookahead.cpp
@@ -574,9 +574,9 @@ namespace sls {
         }
                 
         CTRACE("arith", !m_best_expr, tout << "no move " << t << "\n";);
-        CTRACE("arith", m_best_expr && a.is_int_real(m_best_expr), {
-            var_t v = mk_term(m_best_expr);
-            tout << t << " v" << v << " " << mk_bounded_pp(m_best_expr, m) << " := " << value(v) << " " << m_top_score << "\n";
+        CTRACE("arith", m_best_expr && autil.is_int_real(m_best_expr), {
+            var_t v = a.mk_term(m_best_expr);
+            tout << t << " v" << v << " " << mk_bounded_pp(m_best_expr, m) << " := " << a.value(v) << " " << m_top_score << "\n";
             });
         return !!m_best_expr;
     }
@@ -676,7 +676,7 @@ namespace sls {
         a.m_config.max_moves = a.m_stats.m_steps + a.m_config.max_moves_base;
         TRACE("arith", tout << "search " << a.m_stats.m_steps << " " << a.m_config.max_moves << "\n";);
         IF_VERBOSE(3, verbose_stream() << "lookahead-search steps:" << a.m_stats.m_steps << " max-moves:" << a.m_config.max_moves << "\n");
-        TRACE("arith", display(tout));
+        TRACE("arith", a.display(tout));
 
         while (ctx.rlimit().inc() && a.m_stats.m_steps < a.m_config.max_moves) {
             a.m_stats.m_steps++;