From c8e1e180eaa566b1b8a27df9a9f4c81132f7ffc9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Oct 2022 11:05:50 -0700 Subject: [PATCH] prefix Boolean variables in log with b --- src/sat/smt/euf_internalize.cpp | 2 +- src/sat/smt/euf_solver.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 337e95ddf..c0b2540ea 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -174,7 +174,7 @@ namespace euf { lit = lit2; } - TRACE("euf", tout << "attach v" << v << " " << mk_bounded_pp(e, m) << "\n";); + TRACE("euf", tout << "attach b" << v << " " << mk_bounded_pp(e, m) << "\n";); m_bool_var2expr.reserve(v + 1, nullptr); if (m_bool_var2expr[v] && m_egraph.find(e)) { if (m_egraph.find(e)->bool_var() != v) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 5086dea98..149e3b1a2 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -647,10 +647,10 @@ namespace euf { for (auto const& [e, generation, v] : m_reinit) replay.m.insert(e, v); - TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";); + TRACE("euf", for (auto const& kv : replay.m) tout << "b" << kv.m_value << "\n";); for (auto const& [e, generation, v] : m_reinit) { scoped_generation _sg(*this, generation); - TRACE("euf", tout << "replay: " << v << " " << e->get_id() << " " << mk_bounded_pp(e, m) << " " << si.is_bool_op(e) << "\n";); + TRACE("euf", tout << "replay: b" << v << " #" << e->get_id() << " " << mk_bounded_pp(e, m) << " " << si.is_bool_op(e) << "\n";); sat::literal lit; if (si.is_bool_op(e)) lit = literal(replay.m[e], false);