From 071c9abd694290eb7279219d22d99a6231eac30d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2025 10:59:11 -0800 Subject: [PATCH] Update macro_finder.cpp move to justified_expr --- src/ast/macros/macro_finder.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index 3006e383c..a715d1241 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -346,8 +346,8 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect m_macro_manager.display(tout);); bool found_new_macro = false; for (unsigned i = 0; i < num; i++) { - expr * n = fmls[i].get_fml(); - proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : nullptr; + expr * n = fmls[i].fml(); + proof * pr = m.proofs_enabled() ? fmls[i].pr() : nullptr; expr_ref new_n(m), def(m); proof_ref new_pr(m); expr_dependency_ref new_dep(m);