mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Remove stale monadic statistics declarations

Browse source 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554
This commit is contained in:
Nikolaj Bjorner 2026-08-02 14:32:29 -07:00
parent 0c251e2930
commit 4b2e69c660
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/seq_monadic.h
View file

@ -113,7 +113,6 @@ private:
unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops)
bool m_giveup = false; // set when the budget is exhausted
config m_config;
statistics m_stats;
obj_map<expr, expr*> m_model; // last extracted model (var -> witness); see get_model()
cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above)
guard_set::cache m_rp_cache; // cofactor guard -> range predicate
@ -206,8 +205,6 @@ public:
transition_mode mode() const { return m_config.m_mode; }
void collect_statistics(::statistics& st) const;
// Enable/disable model generation (default: enabled). When enabled, a successful
// solve()/check() extracts a feasible model retrievable via get_model().
void set_gen_model(bool b) { m_config.m_model = b; }