mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

Fix TRACE macro: use unquoted tag identifier (purify_arith not "purify_arith")

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-12 17:55:43 +00:00
parent af6f89217c
commit 8c0ea9f0e7
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/purify_arith_simplifier.h
View file

@ -174,7 +174,7 @@ class purify_arith_simplifier : public dependent_expr_simplifier {
void push_cnstr(expr * cnstr) {
m_new_cnstrs.push_back(cnstr);
TRACE("purify_arith", tout << mk_pp(cnstr, m()) << "\n";);
TRACE(purify_arith, tout << mk_pp(cnstr, m()) << "\n";);
}
void cache_result(app * t, expr * r, proof * pr) {
@ -540,7 +540,7 @@ class purify_arith_simplifier : public dependent_expr_simplifier {
expr_ref new_body(m());
proof_ref new_body_pr(m());
r(q->get_expr(), new_body, new_body_pr);
TRACE("purify_arith",
TRACE(purify_arith,
tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << new_body << "\n";);
result = m().update_quantifier(q, new_body);
}