From f02fbb49bb7ecb34a561fcab51e11f7cd46067d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 13:00:52 -0700 Subject: [PATCH] fix #5253 --- src/sat/smt/q_mam.cpp | 14 ++++---------- src/smt/mam.cpp | 14 +++++--------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index a73df33ae..6a7b8e1e4 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -1224,16 +1224,10 @@ namespace q { m_mp_already_processed[first_idx] = true; linearise_multi_pattern(first_idx); } - -#ifdef Z3DEBUG - for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { - CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; - tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; - tout << "tree:\n" << *m_tree << "\n"; - ); - SASSERT(m_vars[i] >= 0); - } -#endif + for (unsigned i = 0; i < m_qa->get_num_decls(); i++) + if (m_vars[i] == -1) + return; + SASSERT(head->m_next == 0); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin()))); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 0e5764539..25fe5c43d 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1218,15 +1218,11 @@ namespace { linearise_multi_pattern(first_idx); } -#ifdef Z3DEBUG - for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { - CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; - tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; - tout << "tree:\n" << *m_tree << "\n"; - ); - SASSERT(m_vars[i] >= 0); - } -#endif + // check that all variables are captured by pattern. + for (unsigned i = 0; i < m_qa->get_num_decls(); i++) + if (m_vars[i] == -1) + return; + SASSERT(head->m_next == 0); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin())));