mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

fix concat_axiom loop in propagate(): compare against size()......

Browse source
This commit is contained in:
Murphy Berzish 2015-10-18 19:39:55 -04:00
parent b494804c9c
commit e521ab2c3a
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -376,7 +376,7 @@ void theory_str::propagate() {
} }
m_str_eq_todo.reset(); m_str_eq_todo.reset();
for (unsigned i = 0; i < m_concat_axiom_todo.empty(); ++i) { for (unsigned i = 0; i < m_concat_axiom_todo.size(); ++i) {
instantiate_concat_axiom(m_concat_axiom_todo[i]); instantiate_concat_axiom(m_concat_axiom_todo[i]);
} }
m_concat_axiom_todo.reset(); m_concat_axiom_todo.reset();