From e9cff33feb45db366cce824b96ad3ec1df0ea3f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 May 2022 11:24:58 -0700 Subject: [PATCH] fix #5068 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/sat_th.cpp | 3 ++- src/sat/smt/sat_th.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 2cbba7589..6167d3b9b 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -244,8 +244,9 @@ namespace euf { m_eqs = reinterpret_cast(base_ptr); for (i = 0; i < n_eqs; ++i) m_eqs[i] = eqs[i]; - base_ptr += sizeof(enode_pair) * n_eqs; + base_ptr += sizeof(enode_pair) * n_eqs; m_pragma = reinterpret_cast(base_ptr); + i = 0; if (pma) { std::string s = pma->to_string(); for (i = 0; s[i]; ++i) diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 879049497..8e1ab571d 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -220,7 +220,7 @@ namespace euf { unsigned m_num_eqs; sat::literal* m_literals; enode_pair* m_eqs; - char* m_pragma; + char* m_pragma = nullptr; static size_t get_obj_size(unsigned num_lits, unsigned num_eqs, sat::proof_hint const* pma); th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, sat::proof_hint const* pma = nullptr); static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, sat::proof_hint const* pma = nullptr);