From d7472f0726ee9d198a0008b8afd0b0e2e425678a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jul 2022 12:48:21 -0700 Subject: [PATCH] fix #6124 expression pointers were changed within a function, but not pinned. So the pointers got stale. To enforce their life-time within the function body (for use in logging) pin the expressions. --- src/smt/theory_arith_core.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index c7a92b18c..808984521 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -492,6 +492,7 @@ namespace smt { void theory_arith::mk_axiom(expr * ante, expr * conseq, bool simplify_conseq) { th_rewriter & s = ctx.get_rewriter(); expr_ref s_ante(m), s_conseq(m); + expr_ref p_ante(ante, m), p_conseq(conseq, m); // pinned versions expr* s_conseq_n, * s_ante_n; bool negated;