From dd91cfb47e309e1f2b8a11581390cea4f22a82bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Aug 2021 22:21:52 -0700 Subject: [PATCH] #5482 update temp variables --- src/sat/smt/q_mam.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 8b75e87ea..bd8859575 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -3344,8 +3344,8 @@ namespace q { update_plbls(lbl2); update_pp(m_lbl_hasher(lbl1), m_lbl_hasher(lbl2), curr_path, p, qa, mp); } - if (!found) - var_paths.push_back(p); + if (!found) + var_paths.push_back(p); } enode * get_ground_arg(app * pat, quantifier * qa, unsigned & pos) { @@ -3413,7 +3413,7 @@ namespace q { unsigned num_vars = qa->get_num_decls(); if (num_vars >= m_var_paths.size()) 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_tmp_region.reset(); // Given a multi-pattern (p_1, ..., p_n)