From c2e73a6aaee3ec5a3cd5758046c14fedefc97e95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:19:28 -0700 Subject: [PATCH] logging pre-processing Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index d70d232e4..0c4c2a7b6 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -110,12 +110,13 @@ class simplifier_solver : public solver { expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); if (qhead < m_fmls.size() || !assumptions.empty()) { - TRACE("solver", tout << "qhead " << qhead << "\n"); m_preprocess_state.replay(qhead, assumptions); m_preprocess_state.freeze(assumptions); m_preprocess.reduce(); if (!m.inc()) return; + TRACE("solver", tout << "qhead " << qhead << "\n"; + m_preprocess_state.display(tout)); m_preprocess_state.advance_qhead(); for (unsigned i = 0; i < assumptions.size(); ++i) m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));