diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 8e548e678..6eb070b7c 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -199,7 +199,8 @@ namespace smt {
         };
         lit_node* m_dll_lits;
 
-        svector<std::array<double, 2>> m_lit_scores; 
+
+        svector<double> m_lit_scores[2];
 
         clause_vector               m_aux_clauses;
         clause_vector               m_lemmas;
@@ -947,11 +948,14 @@ namespace smt {
         void dump_axiom(unsigned n, literal const* lits);
         void add_scores(unsigned n, literal const* lits);
         void reset_scores() {
-            for (auto& s : m_lit_scores) s[0] = s[1] = 0.0;
+            for (auto& e : m_lit_scores[0])
+                e = 0;
+            for (auto& e : m_lit_scores[1])
+                e = 0;
             m_pq_scores.clear();  // Clear the priority queue heap as well
         }
         double get_score(literal l) const {
-            return m_lit_scores[l.var()][l.sign()];
+            return m_lit_scores[l.sign()][l.var()];
         }
     public:        
 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index ecb56e516..c7e257fac 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -931,8 +931,10 @@ namespace smt {
         set_bool_var(id, v);
         m_bdata.reserve(v+1);
         m_activity.reserve(v+1);
-        m_lit_scores.reserve(v + 1);
-        m_lit_scores[v][0] = m_lit_scores[v][1] = 0.0;
+            m_lit_scores[0].reserve(v + 1);
+            m_lit_scores[1].reserve(v + 1);
+
+        m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
         m_bool_var2expr.reserve(v+1);
         m_bool_var2expr[v] = n;
         literal l(v, false);
@@ -1543,10 +1545,9 @@ namespace smt {
             auto lit = lits[i];
             unsigned v = lit.var(); // unique key per literal
 
-            auto curr_score = m_lit_scores[v][0] * m_lit_scores[v][1];
-            m_lit_scores[v][lit.sign()] += 1.0 / n;
+            m_lit_scores[lit.sign()][v] += 1.0 / n;
             
-            auto new_score = m_lit_scores[v][0] * m_lit_scores[v][1];
+            auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
             m_pq_scores.set(v, new_score);
 
         }
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index ce8b699aa..40954437f 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -97,16 +97,6 @@ namespace smt {
         }
 
 
-        auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
-            lookahead lh(ctx);
-            c = lh.choose();
-            if (c) {
-                if ((ctx.get_random_value() % 2) == 0) 
-                    c = c.get_manager().mk_not(c);
-                lasms.push_back(c);
-            }
-        };
-
         auto cube_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
             unsigned k = 3; // Number of top literals you want
 
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 07b04019d..b1c5aa6b5 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -24,6 +24,22 @@ namespace smt {
 
     class parallel {
         context& ctx;
+
+        class worker {
+            ast_manager m;
+            context ctx;
+            expr_ref_vector asms;
+        public:
+            worker(context& ctx, expr_ref_vector const& asms);
+            void run();
+            void cancel();
+        };
+
+        std::mutex mux;
+        void set_unsat();
+        void set_sat(ast_translation& tr, model& m);
+        void get_cubes(ast_translation& tr, expr_ref_vector& cubes);
+
     public:
         parallel(context& ctx): ctx(ctx) {}