mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix #6124

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2022-07-05 12:48:21 -07:00
parent f82ca197d2
commit d7472f0726
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_arith_core.h
View file

@ -492,6 +492,7 @@ namespace smt {
void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq, bool simplify_conseq) { void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq, bool simplify_conseq) {
th_rewriter & s = ctx.get_rewriter(); th_rewriter & s = ctx.get_rewriter();
expr_ref s_ante(m), s_conseq(m); 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; expr* s_conseq_n, * s_ante_n;
bool negated; bool negated;