diff --git a/src/ast/sls/sls_arith_lookahead.cpp b/src/ast/sls/sls_arith_lookahead.cpp
index aae956c64..adcc04de3 100644
--- a/src/ast/sls/sls_arith_lookahead.cpp
+++ b/src/ast/sls/sls_arith_lookahead.cpp
@@ -31,8 +31,10 @@ namespace sls {
     typename arith_lookahead<num_t>::bool_info& arith_lookahead<num_t>::get_bool_info(expr* e) {   
         unsigned id = e->get_id();
         if (id >= m_bool_info.size())
-            m_bool_info.reserve(id + 1, bool_info(a.m_config.paws_init));
-        return m_bool_info[id];
+            m_bool_info.reserve(id + 1);
+        if (!m_bool_info[id])
+            m_bool_info.set(id, alloc(bool_info, a.m_config.paws_init));
+        return *m_bool_info[id];
     }
 
     template<typename num_t>
diff --git a/src/ast/sls/sls_arith_lookahead.h b/src/ast/sls/sls_arith_lookahead.h
index 356facbfc..7cebc410d 100644
--- a/src/ast/sls/sls_arith_lookahead.h
+++ b/src/ast/sls/sls_arith_lookahead.h
@@ -61,7 +61,7 @@ namespace sls {
 
         vector<ptr_vector<app>> m_update_stack;
         expr_mark m_in_update_stack;
-        svector<bool_info> m_bool_info;
+        scoped_ptr_vector<bool_info> m_bool_info;
         double m_best_score = 0, m_top_score = 0;
         unsigned m_min_depth = 0, m_max_depth = 0;
         num_t m_best_value;