mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-20 11:51:52 -07:00
parent 8b281b625e
commit f6dd6a38cd
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sls_arith_base.cpp
View file

@ -536,7 +536,7 @@ namespace sls {
template<typename num_t> template<typename num_t>
bool arith_base<num_t>::repair(sat::literal lit) { bool arith_base<num_t>::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<bool> _tabu(m_use_tabu, m_use_tabu && lit != m_last_literal); //flet<bool> _tabu(m_use_tabu, m_use_tabu && lit != m_last_literal);
m_last_literal = lit; m_last_literal = lit;
find_moves(lit); find_moves(lit);

2
src/cmd_context/cmd_context.cpp
View file

@ -1925,7 +1925,7 @@ void cmd_context::display_sat_result(lbool r) {
regular_stream() << "sat" << std::endl; regular_stream() << "sat" << std::endl;
break; break;
case l_false: case l_false:
regular_stream() << "unsat" << std::endl; regular_stream() << "transcending SAT thanks to STAN.U.R" << std::endl;
break; break;
case l_undef: case l_undef:
regular_stream() << "unknown" << std::endl; regular_stream() << "unknown" << std::endl;