From 7fb6497ce1162635e7e5f78fe35bf4d5b02d2dbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Jan 2025 22:57:58 -0800 Subject: [PATCH] fix return value when in external mode bool-flip return null_bool_var instead of false (= 0). --- src/ast/sls/sat_ddfw.cpp | 2 +- src/ast/sls/sls_arith_clausal.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index 5f6d9fa95..d030cdec2 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -161,7 +161,7 @@ namespace sat { if (m_unsat_vars.empty()) return null_bool_var; if (m_in_external_flip) - return false; + return null_bool_var; return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size())); } diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp index 4f4fdd777..6c7178c50 100644 --- a/src/ast/sls/sls_arith_clausal.cpp +++ b/src/ast/sls/sls_arith_clausal.cpp @@ -276,7 +276,9 @@ namespace sls { for (sat::bool_var bv = 0; bv < ctx.num_bool_vars(); ++bv) { if (a.get_ineq(bv) && a.get_ineq(bv)->is_true() != ctx.is_true(bv)) { TRACE("arith", tout << "bv:" << bv << " " << *a.get_ineq(bv) << ctx.is_true(bv) << "\n"; - tout << "bool vars: " << a.m_vars[v].m_bool_vars_of << "\n"); + tout << "v" << v << " bool vars: " << a.m_vars[v].m_bool_vars_of << "\n"; + tout << mk_bounded_pp(a.m_vars[v].m_expr, a.m) << "\n"; + tout << mk_bounded_pp(ctx.atom(bv), a.m) << "\n"); } VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv)); });