From 38d526ee4505c9109ecdc9e1f134946539c4e3a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2023 10:18:03 -0800 Subject: [PATCH] fix warning Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/eliminate_predicates.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index 2166913da..6c1eccea0 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -567,9 +567,9 @@ void eliminate_predicates::try_find_macro(clause& cl) { return false; app* x = to_app(_x); return - can_be_quasi_macro_head(x, cl.m_bound.size()) && - is_macro_safe(y) && - !occurs(x->get_decl(), y); + can_be_quasi_macro_head(x, cl.m_bound.size()) && + is_macro_safe(y) && + !occurs(x->get_decl(), y); }; if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) { @@ -592,7 +592,8 @@ void eliminate_predicates::try_find_macro(clause& cl) { } if (cl.is_unit()) { expr* body = cl.sign(0) ? m.mk_false() : m.mk_true(); - if (can_be_qdef(cl.atom(0), body)) { + expr* x = cl.atom(0); + if (can_be_qdef(x, body)) { insert_quasi_macro(to_app(x), body, cl); return; }