From 7566cc744d3aff13ced687104b2cb5bff1a1472b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Sep 2025 19:03:22 -0700 Subject: [PATCH] display assumptions used --- src/smt/smt_solver.cpp | 2 +- src/solver/solver_na2as.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 1d38c0685..0fcb5b702 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -196,7 +196,7 @@ namespace { } lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { - TRACE(solver_na2as, tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";); + TRACE(solver_na2as, tout << "smt_solver::check_sat_core:\n"; for (unsigned i = 0; i < num_assumptions; ++i) tout << mk_pp(assumptions[i], m) << "\n";); return m_context.check(num_assumptions, assumptions); } diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index e3e49ef01..2f1d05a13 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -61,7 +61,7 @@ struct append_assumptions { lbool solver_na2as::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { append_assumptions app(m_assumptions, num_assumptions, assumptions); - TRACE(solver_na2as, display(tout);); + TRACE(solver_na2as, display(tout, m_assumptions.size(), m_assumptions.data());); return check_sat_core2(m_assumptions.size(), m_assumptions.data()); }