summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/conjecture_generator.cpp
diff options
context:
space:
mode:
authorPaul Meng <baolmeng@gmail.com>2016-10-11 13:54:20 -0500
committerPaul Meng <baolmeng@gmail.com>2016-10-11 13:54:20 -0500
commit3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch)
tree0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/quantifiers/conjecture_generator.cpp
parent773e7d27d606b71ff0f78e84efe1deef2653f016 (diff)
parent5f415d4585134612bc24e9a823289fee35541a01 (diff)
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts: src/options/quantifiers_options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rwxr-xr-xsrc/theory/quantifiers/conjecture_generator.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f4eb67d74..11adc61fd 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -84,6 +84,9 @@ d_notify( *this ),
d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
d_ee_conjectures( c ){
d_fullEffortCount = 0;
+ d_conj_count = 0;
+ d_subs_confirmCount = 0;
+ d_subs_unkCount = 0;
d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback