From 710f75749521c212a9f08a2e04d3fa3fe07c60b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Jan 2025 15:57:02 -0800
Subject: [PATCH] fixup parameter handling for enabling bv-lookahead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_lookahead.cpp | 5 ++++-
 src/ast/sls/sls_bv_lookahead.h   | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 2e9c1949a..26e0645b5 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -52,6 +52,8 @@ namespace sls {
 
     void bv_lookahead::search() {
         updt_params(ctx.get_params());
+        if (!m_config.use_lookahead_bv)
+            return;
         initialize_bool_values();
         rescore();
         m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
@@ -263,7 +265,7 @@ namespace sls {
         if (0x1 == (m_stats.m_restarts & 0x1))
             m_config.restart_next += m_config.restart_base;
         else
-            m_config.restart_next += (2 << (m_stats.m_restarts >> 1)) * m_config.restart_base;
+            m_config.restart_next += (2 * (m_stats.m_restarts >> 1)) * m_config.restart_base;
 
         reset_uninterp_in_false_literals(); 
         rescore();
@@ -328,6 +330,7 @@ namespace sls {
         m_config.ucb_init = p.walksat_ucb_init();
         m_config.ucb_noise = p.walksat_ucb_noise();
         m_config.use_top_level_assertions = p.use_top_level_assertions_bv();
+        m_config.use_lookahead_bv = p.use_lookahead_bv();
     }
 
     /**
diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
index def61b9e7..8c3de7d24 100644
--- a/src/ast/sls/sls_bv_lookahead.h
+++ b/src/ast/sls/sls_bv_lookahead.h
@@ -47,6 +47,7 @@ namespace sls {
             bool ucb_init = false;
             double ucb_noise = 0.1;
             bool   use_top_level_assertions = true;
+            bool   use_lookahead_bv = true;
         };
 
         struct stats {