summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-01-10 10:50:56 -0600
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-01-10 10:50:56 -0600
commit21f8e233e46fae32eaa6d2d4d5b4d0f36c36ba7f (patch)
tree610112b7b9f621466e478f29997a8fe2d5a62ccb /src/theory/quantifiers/model_engine.h
parent841b7951f41f399859afab13a81e04599308da61 (diff)
Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
-rw-r--r--src/theory/quantifiers/model_engine.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index fcbba7aee..ba54d7ba4 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -68,6 +68,7 @@ public:
public:
IntStat d_inst_rounds;
IntStat d_exh_inst_lemmas;
+ IntStat d_mbqi_inst_lemmas;
Statistics();
~Statistics();
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback