mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix use-after-free

Browse source
This commit is contained in:
Murphy Berzish 2018-03-19 23:09:07 -04:00
parent d26eddf776
commit 7759d05efe
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str.cpp
View file

@ -803,8 +803,20 @@ namespace smt {
context & ctx = get_context();
while (can_propagate()) {
TRACE("str", tout << "propagating..." << std::endl;);
for (auto const& el : m_basicstr_axiom_todo) {
instantiate_basic_string_axioms(el);
while(true) {
// this can potentially recursively activate itself
unsigned start_count = m_basicstr_axiom_todo.size();
ptr_vector<enode> axioms_tmp(m_basicstr_axiom_todo);
for (auto const& el : axioms_tmp) {
instantiate_basic_string_axioms(el);
}
unsigned end_count = m_basicstr_axiom_todo.size();
if (end_count > start_count) {
TRACE("str", tout << "new basic string axiom terms added -- checking again" << std::endl;);
continue;
} else {
break;
}
}
m_basicstr_axiom_todo.reset();
TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);