mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-10 10:50:42 -07:00
parent 9c9cd5ebf7
commit 82658d1bce
1 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_dense_diff_logic_def.h
View file

@ -55,10 +55,8 @@ namespace smt {
bool is_int = m_autil.is_int(n->get_owner()); bool is_int = m_autil.is_int(n->get_owner());
m_is_int.push_back(is_int); m_is_int.push_back(is_int);
m_f_targets.push_back(f_target()); m_f_targets.push_back(f_target());
typename matrix::iterator it = m_matrix.begin(); for (auto& rows : m_matrix) {
typename matrix::iterator end = m_matrix.end(); rows.push_back(cell());
for (; it != end; ++it) {
it->push_back(cell());
} }
m_matrix.push_back(row()); m_matrix.push_back(row());
row & r = m_matrix.back(); row & r = m_matrix.back();
@ -367,10 +365,8 @@ namespace smt {
m_is_int.shrink(old_num_vars); m_is_int.shrink(old_num_vars);
m_f_targets.shrink(old_num_vars); m_f_targets.shrink(old_num_vars);
m_matrix.shrink(old_num_vars); m_matrix.shrink(old_num_vars);
typename matrix::iterator it = m_matrix.begin(); for (auto& cells : m_matrix) {
typename matrix::iterator end = m_matrix.end(); cells.shrink(old_num_vars);
for (; it != end; ++it) {
it->shrink(old_num_vars);
} }
} }
} }