summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/candidate_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/candidate_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/candidate_generator.cpp')
-rwxr-xr-xsrc/theory/quantifiers/candidate_generator.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index a0d9bda0f..8e8f34cac 100755
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
Assert( mpat.getKind()==INST_CONSTANT );
d_f = quantifiers::TermDb::getInstConstAttr( mpat );
d_index = mpat.getAttribute(InstVarNumAttribute());
+ d_firstTime = false;
}
void CandidateGeneratorQEAll::resetInstantiationRound() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback