summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h10
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 5fca96f0d..91c21a650 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -247,17 +247,7 @@ public:
IntStat d_triggers;
IntStat d_simple_triggers;
IntStat d_multi_triggers;
- IntStat d_multi_trigger_instantiations;
IntStat d_red_alpha_equiv;
- IntStat d_instantiations_user_patterns;
- IntStat d_instantiations_auto_gen;
- IntStat d_instantiations_guess;
- IntStat d_instantiations_qcf;
- IntStat d_instantiations_qcf_prop;
- IntStat d_instantiations_fmf_exh;
- IntStat d_instantiations_fmf_mbqi;
- IntStat d_instantiations_cbqi;
- IntStat d_instantiations_rr;
Statistics();
~Statistics();
};/* class QuantifiersEngine::Statistics */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback