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

call into collect_statistics in case of -T interrupt

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-01 14:15:15 -07:00
parent a28f55a3bc
commit 97193b4a1d
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/solver/tactic2solver.cpp
View file

@ -309,6 +309,8 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
void tactic2solver::collect_statistics(statistics & st) const { void tactic2solver::collect_statistics(statistics & st) const {
st.copy(m_stats); st.copy(m_stats);
if (m_stats.size() == 0 && m_tactic)
m_tactic->collect_statistics(st);
//SASSERT(m_stats.size() > 0); //SASSERT(m_stats.size() > 0);
} }