mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 20:59:01 +00:00
Code Activity

display assumptions used

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-07 19:03:22 -07:00
parent e6b0b2d1b4
commit 7566cc744d
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_solver.cpp
View file

@ -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);
}

2
src/solver/solver_na2as.cpp
View file

@ -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());
}