From af2cc460a96b6db97c774ef0b8926c145f26d216 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Nov 2021 08:52:48 -0700 Subject: [PATCH] #5646 --- src/smt/theory_recfun.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 1a2bf0049..1bf987008 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -254,14 +254,16 @@ namespace smt { ctx.internalize_assertions(); lit = mk_literal(fn); } - else if (m.is_true(r) || m.is_false(r)) - std::swap(l, r); - else if (m.is_true(l)) - lit = mk_literal(r); - else if (m.is_false(l)) - lit = ~mk_literal(r); - else - lit = mk_eq(l, r, false); + else { + if (m.is_true(r) || m.is_false(r)) + std::swap(l, r); + if (m.is_true(l)) + lit = mk_literal(r); + else if (m.is_false(l)) + lit = ~mk_literal(r); + else + lit = mk_eq(l, r, false); + } ctx.mark_as_relevant(lit); return lit; }