From 5250c3b9edf8b4d6d05478ad86adcbb311cc48e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 May 2016 09:37:15 -0700 Subject: [PATCH] ensure reference ownership on frame elements to avoid crashes due to nnf. Issue #588 Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/nnf.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 6b10e8c10..e15e26bf2 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -200,14 +200,14 @@ typedef default_exception nnf_exception; struct nnf::imp { struct frame { - expr * m_curr; + expr_ref m_curr; unsigned m_i:28; unsigned m_pol:1; // pos/neg polarity unsigned m_in_q:1; // true if m_curr is nested in a quantifier unsigned m_new_child:1; unsigned m_cache_result:1; unsigned m_spos; // top of the result stack, when the frame was created. - frame(expr * n, bool pol, bool in_q, bool cache_res, unsigned spos): + frame(expr_ref& n, bool pol, bool in_q, bool cache_res, unsigned spos): m_curr(n), m_i(0), m_pol(pol), @@ -225,7 +225,7 @@ struct nnf::imp { #define POS_Q_CIDX 3 // positive polarity and nested in a quantifier ast_manager & m_manager; - svector m_frame_stack; + vector m_frame_stack; expr_ref_vector m_result_stack; typedef act_cache cache; @@ -324,7 +324,8 @@ struct nnf::imp { } void push_frame(expr * t, bool pol, bool in_q, bool cache_res) { - m_frame_stack.push_back(frame(t, pol, in_q, cache_res, m_result_stack.size())); + expr_ref tr(t, m()); + m_frame_stack.push_back(frame(tr, pol, in_q, cache_res, m_result_stack.size())); } static unsigned get_cache_idx(bool pol, bool in_q) {