From 09e84e04487fc539a4d9c610c7223621ef6ce0b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Jan 2025 07:28:14 -0800 Subject: [PATCH] fix crash when accessing bool-info vars, reported by Clemens Eisenhofer Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_lookahead.cpp | 6 ++++-- src/ast/sls/sls_arith_lookahead.h | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) 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::bool_info& arith_lookahead::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 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> m_update_stack; expr_mark m_in_update_stack; - svector m_bool_info; + scoped_ptr_vector 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;