From 9bba708f9b34300be3e1252b3948549b5eec1e20 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 25 Jul 2025 15:36:37 -0700
Subject: [PATCH] fix compilation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.h        | 2 +-
 src/smt/smt_internalizer.cpp | 7 ++++---
 src/smt/smt_parallel.cpp     | 3 +++
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index da6e92569..352ea7111 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -189,7 +189,7 @@ namespace smt {
         unsigned_vector             m_lit_occs;    //!< occurrence count of literals
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
-        svector<double[2]>          m_scores;
+        svector<double>             m_scores[2];
         clause_vector               m_aux_clauses;
         clause_vector               m_lemmas;
         vector<clause_vector>       m_clauses_to_reinit;
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index faf7ea24d..9a04741e2 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -928,8 +928,9 @@ namespace smt {
         set_bool_var(id, v);
         m_bdata.reserve(v+1);
         m_activity.reserve(v+1);
-        m_scores.reserve(v + 1);
-        m_scores[v][0] = m_scores[v][1] = 0.0;
+        m_scores[0].reserve(v + 1);
+        m_scores[1].reserve(v + 1);
+        m_scores[0][v] = m_scores[1][v] = 0.0;
         m_bool_var2expr.reserve(v+1);
         m_bool_var2expr[v] = n;
         literal l(v, false);
@@ -1531,7 +1532,7 @@ namespace smt {
         for (unsigned i = 0; i < n; ++i) {
             auto lit = lits[i];
             unsigned v = lit.var();
-            m_scores[v][lit.sign()] += 1.0 / n;
+            m_scores[lit.sign()][v] += 1.0 / n;
         }
     }
 
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index ac5a81979..8e07ed492 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -92,6 +92,9 @@ namespace smt {
             sl.push_child(&(new_m->limit()));
         }
 
+        // Access socres as follows:
+        // ctx.m_scores[lit.sign()][lit.var()]
+
         // auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
         //     lookahead lh(ctx);
         //     c = lh.choose();