diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-13 23:08:40 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-13 23:24:12 +0100 |
| commit | 94fe6a0d525bff3cdd4450b2abd04eb2cb044308 (patch) | |
| tree | 948461ad09772d5e2612b1fbf1d384360c0a29a7 /src/theory/quantifiers_engine.cpp | |
| parent | 3a973bd4fb586707a20d5e73146b79ff9fd6a77a (diff) | |
Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3813d7cd2..e7a87927a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -95,6 +95,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; d_hasAddedLemma = false; + //don't add true lemma + d_lemmas_produced_c[d_term_db->d_true] = true; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; |