mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add logging and diagnostics

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-09 19:50:22 -08:00
parent 9d09064ad0
commit f4e17ecc65
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.cpp
View file

@ -282,6 +282,7 @@ namespace sat {
m_model_is_current = false; m_model_is_current = false;
m_stats.m_mk_var++; m_stats.m_mk_var++;
bool_var v = m_justification.size(); bool_var v = m_justification.size();
if (!m_free_vars.empty()) { if (!m_free_vars.empty()) {
v = m_free_vars.back(); v = m_free_vars.back();
m_free_vars.pop_back(); m_free_vars.pop_back();
@ -1262,6 +1263,7 @@ namespace sat {
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
if (m_config.m_force_cleanup) do_cleanup(true); if (m_config.m_force_cleanup) do_cleanup(true);
TRACE("sat", display(tout);); TRACE("sat", display(tout););
TRACE("before_search", display(tout););
if (m_config.m_gc_burst) { if (m_config.m_gc_burst) {
// force gc // force gc

2
src/solver/assertions/asserted_formulas.cpp
View file

@ -279,6 +279,8 @@ void asserted_formulas::reduce() {
TRACE("before_reduce", display(tout);); TRACE("before_reduce", display(tout););
CASSERT("well_sorted", check_well_sorted()); CASSERT("well_sorted", check_well_sorted());
IF_VERBOSE(10, verbose_stream() << "(smt.simplify-begin :num-exprs " << get_total_size() << ")\n";);
set_eliminate_and(false); // do not eliminate and before nnf. set_eliminate_and(false); // do not eliminate and before nnf.
if (!invoke(m_propagate_values)) return; if (!invoke(m_propagate_values)) return;
if (!invoke(m_find_macros)) return; if (!invoke(m_find_macros)) return;