diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp
index 0256646db..801c97653 100644
--- a/src/smt/smt_lookahead.cpp
+++ b/src/smt/smt_lookahead.cpp
@@ -18,7 +18,8 @@ Revision History:
 --*/
 
 #include <cmath>
-#include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "smt/smt_lookahead.h"
 #include "smt/smt_context.h"
 
@@ -78,7 +79,7 @@ namespace smt {
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);
         
-        unsigned nf = 0, nc = 0, ns = 0, bound = 2000;
+        unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
         for (bool_var v : vars) {
             if (!ctx.bool_var2expr(v)) continue;
             literal lit(v, false);			
@@ -108,7 +109,9 @@ namespace smt {
                 continue;
             }
             double score = score1 + score2 + 1024*score1*score2;
-            if (score > best_score) {
+
+            if (score > best_score || (score == best_score && ctx.get_random_value() % (++n) == 0)) {
+                if (score > best_score) n = 0;
                 best_score = score;
                 best_v = v;
                 bound += ns;
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 876435163..381e18d1a 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -17,6 +17,7 @@ Author:
 
 #include "util/scoped_ptr_vector.h"
 #include "ast/ast_util.h"
+#include "ast/ast_pp.h"
 #include "ast/ast_translation.h"
 #include "smt/smt_parallel.h"
 #include "smt/smt_lookahead.h"
@@ -115,7 +116,7 @@ namespace smt {
                 }
                 IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; 
                            if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
-                           if (c) verbose_stream() << " :cube: " << c;
+                           if (c) verbose_stream() << " :cube: " << mk_pp(c, pm);
                            verbose_stream() << ")\n";);
                 lbool r = pctx.check(lasms.size(), lasms.c_ptr());