diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
commit | 433401b05664d9c8827b19455ef7b93fd27efd9d (patch) | |
tree | 9be15c6804521434d4116b05eb571ecd78ac2767 /src/theory/quantifiers_engine.cpp | |
parent | fc573f3512b5345763755c9d7a061d430c46ae5f (diff) |
Accept user-provided triggers with variable terms. Flush lemmas before quantifiers check. Minor fix for conjecture generation.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a00592e8b..4c29c8f9a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -195,6 +195,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ //reset relevant information d_conflict = false; d_hasAddedLemma = false; + + //flush previous lemmas (for instance, if was interupted) + flushLemmas(); + if( d_hasAddedLemma ){ + return; + } + d_term_db->reset( e ); d_eq_query->reset(); if( d_rel_dom ){ |