summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r--src/theory/quantifiers/instantiation_engine.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 53777d362..a460f1164 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -149,6 +149,7 @@ public:
IntStat d_instantiations_cbqi_arith;
IntStat d_instantiations_cbqi_arith_minus;
IntStat d_instantiations_cbqi_datatypes;
+ IntStat d_instantiation_rounds;
Statistics();
~Statistics();
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback