mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

#5482

Browse source 
update temp variables
This commit is contained in:
Nikolaj Bjorner 2021-08-23 22:21:52 -07:00
parent 592c53e46d
commit dd91cfb47e
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/q_mam.cpp
View file

@ -3344,8 +3344,8 @@ namespace q {
update_plbls(lbl2); update_plbls(lbl2);
update_pp(m_lbl_hasher(lbl1), m_lbl_hasher(lbl2), curr_path, p, qa, mp); update_pp(m_lbl_hasher(lbl1), m_lbl_hasher(lbl2), curr_path, p, qa, mp);
} }
if (!found) if (!found)
var_paths.push_back(p); var_paths.push_back(p);
} }
enode * get_ground_arg(app * pat, quantifier * qa, unsigned & pos) { enode * get_ground_arg(app * pat, quantifier * qa, unsigned & pos) {
@ -3413,7 +3413,7 @@ namespace q {
unsigned num_vars = qa->get_num_decls(); unsigned num_vars = qa->get_num_decls();
if (num_vars >= m_var_paths.size()) if (num_vars >= m_var_paths.size())
m_var_paths.resize(num_vars+1); m_var_paths.resize(num_vars+1);
for (unsigned i = 0; i < num_vars; i++) for (unsigned i = 0; i <= num_vars; i++)
m_var_paths[i].reset(); m_var_paths[i].reset();
m_tmp_region.reset(); m_tmp_region.reset();
// Given a multi-pattern (p_1, ..., p_n) // Given a multi-pattern (p_1, ..., p_n)