mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

fix #4365

Browse source 
m_library_aware_axiom_todo.reset(); should not be called because this vector is owned by the m_library_aware_trail_stack object.
This commit is contained in:
Nikolaj Bjorner 2021-04-10 13:03:05 -07:00
parent f607c15aa2
commit 8d9be5322f
1 changed files with 5 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_str.cpp
View file

@ -7275,7 +7275,6 @@ namespace smt {
m_basicstr_axiom_todo.reset(); m_basicstr_axiom_todo.reset();
m_concat_axiom_todo.reset(); m_concat_axiom_todo.reset();
m_concat_eval_todo.reset(); m_concat_eval_todo.reset();
m_library_aware_axiom_todo.reset();
m_delayed_axiom_setup_terms.reset(); m_delayed_axiom_setup_terms.reset();
m_delayed_assertions_todo.reset(); m_delayed_assertions_todo.reset();
@ -7299,17 +7298,11 @@ namespace smt {
varItor++; varItor++;
} }
if (!cutvarmap_removes.empty()) { for (expr* ex : cutvarmap_removes)
ptr_vector<expr>::iterator it = cutvarmap_removes.begin(); cut_var_map.remove(ex);
for (; it != cutvarmap_removes.end(); ++it) {
expr * ex = *it;
cut_var_map.remove(ex);
}
}
ptr_vector<enode> new_m_basicstr; ptr_vector<enode> new_m_basicstr;
for (ptr_vector<enode>::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) { for (enode* e : m_basicstr_axiom_todo) {
enode * e = *it;
TRACE("str", tout << "consider deleting " << mk_pp(e->get_expr(), get_manager()) TRACE("str", tout << "consider deleting " << mk_pp(e->get_expr(), get_manager())
<< ", enode scope level is " << e->get_iscope_lvl() << ", enode scope level is " << e->get_iscope_lvl()
<< std::endl;); << std::endl;);
@ -7328,6 +7321,8 @@ namespace smt {
} }
m_trail_stack.pop_scope(num_scopes); 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); m_library_aware_trail_stack.pop_scope(num_scopes);
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);