From f6dd6a38cdcba0d4ec367abd4f7da71efb8c1c7e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Aug 2024 11:51:52 -0700 Subject: [PATCH] update Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 2 +- src/cmd_context/cmd_context.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index f452c24a8..8ce608624 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -536,7 +536,7 @@ namespace sls { template bool arith_base::repair(sat::literal lit) { - verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n"; + //verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n"; //flet _tabu(m_use_tabu, m_use_tabu && lit != m_last_literal); m_last_literal = lit; find_moves(lit); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 231c78bc2..b6846a83a 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() << "unsat" << std::endl; + regular_stream() << "transcending SAT thanks to STAN.U.R" << std::endl; break; case l_undef: regular_stream() << "unknown" << std::endl;