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

trace push/pop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-31 14:22:57 -07:00
parent 98d42421bc
commit c7898b1977
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/solver/combined_solver.cpp
View file

@ -187,9 +187,11 @@ public:
switch_inc_mode(); switch_inc_mode();
m_solver1->push(); m_solver1->push();
m_solver2->push(); m_solver2->push();
TRACE("pop", tout << "push\n";);
} }
void pop(unsigned n) override { void pop(unsigned n) override {
TRACE("pop", tout << n << "\n";);
switch_inc_mode(); switch_inc_mode();
m_solver1->pop(n); m_solver1->pop(n);
m_solver2->pop(n); m_solver2->pop(n);

2
src/solver/tactic2solver.cpp
View file

@ -122,9 +122,11 @@ void tactic2solver::assert_expr_core(expr * t) {
void tactic2solver::push_core() { void tactic2solver::push_core() {
m_scopes.push_back(m_assertions.size()); m_scopes.push_back(m_assertions.size());
m_result = nullptr; m_result = nullptr;
TRACE("pop", tout << m_scopes.size() << "\n";);
} }
void tactic2solver::pop_core(unsigned n) { void tactic2solver::pop_core(unsigned n) {
TRACE("pop", tout << m_scopes.size() << " " << n << "\n";);
n = std::min(m_scopes.size(), n); n = std::min(m_scopes.size(), n);
unsigned new_lvl = m_scopes.size() - n; unsigned new_lvl = m_scopes.size() - n;
unsigned old_sz = m_scopes[new_lvl]; unsigned old_sz = m_scopes[new_lvl];