From 8d9be5322f1ddc76244bc855f0e013716074e0ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Apr 2021 13:03:05 -0700 Subject: [PATCH] fix #4365 m_library_aware_axiom_todo.reset(); should not be called because this vector is owned by the m_library_aware_trail_stack object. --- src/smt/theory_str.cpp | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 93ed5464e..544b4807f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7275,7 +7275,6 @@ namespace smt { m_basicstr_axiom_todo.reset(); m_concat_axiom_todo.reset(); m_concat_eval_todo.reset(); - m_library_aware_axiom_todo.reset(); m_delayed_axiom_setup_terms.reset(); m_delayed_assertions_todo.reset(); @@ -7299,17 +7298,11 @@ namespace smt { varItor++; } - if (!cutvarmap_removes.empty()) { - ptr_vector::iterator it = cutvarmap_removes.begin(); - for (; it != cutvarmap_removes.end(); ++it) { - expr * ex = *it; - cut_var_map.remove(ex); - } - } + for (expr* ex : cutvarmap_removes) + cut_var_map.remove(ex); ptr_vector new_m_basicstr; - for (ptr_vector::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) { - enode * e = *it; + for (enode* e : m_basicstr_axiom_todo) { TRACE("str", tout << "consider deleting " << mk_pp(e->get_expr(), get_manager()) << ", enode scope level is " << e->get_iscope_lvl() << std::endl;); @@ -7328,6 +7321,8 @@ namespace smt { } m_trail_stack.pop_scope(num_scopes); + // m_library_aware_trail_stack owns m_library_aware_todo vector. + // the vector cannot be reset outside. m_library_aware_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes);