From a2b8b724b2b1689ae87db16029804d5c6ee056b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Aug 2024 09:20:11 -0700 Subject: [PATCH] fixes to semantics Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 8 ++++---- src/cmd_context/cmd_context.cpp | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index f01d98a7d..c9fc89b89 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -595,19 +595,19 @@ br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind return BR_FAILED; expr_ref f2 = remove_factor(f, arg1); expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1)); + result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z)); switch (kind) { case EQ: - result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z)); break; case GE: - result = m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)); + result = m.mk_or(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)), result); break; case LE: - result = m.mk_xor(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)); + result = m.mk_or(m.mk_not(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z))), result); break; } - return BR_REWRITE2; + return BR_REWRITE3; } return BR_FAILED; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index b6846a83a..231c78bc2 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1925,7 +1925,7 @@ void cmd_context::display_sat_result(lbool r) { regular_stream() << "sat" << std::endl; break; case l_false: - regular_stream() << "transcending SAT thanks to STAN.U.R" << std::endl; + regular_stream() << "unsat" << std::endl; break; case l_undef: regular_stream() << "unknown" << std::endl;