fix sets eager lemmas

diff --git a/src/theory/sets/options b/src/theory/sets/options
index dc6c6e907c524bdd3064a1d28cf565c208d00896..1c95e78e4b2ef5e38cae0968bd4663b01f13dd7d 100644 (file)
--- a/src/theory/sets/options
+++ b/src/theory/sets/options
@@ -8,7 +8,7 @@ module SETS "theory/sets/options.h" Sets
 option setsPropagate --sets-propagate bool :default true
  determines whether to propagate learnt facts to Theory Engine / SAT solver
 
-option setsEagerLemmas --sets-eager-lemmas bool :default false
- if true, will add lemmas even if not at FULL_EFFORT
+option setsEagerLemmas --sets-eager-lemmas bool :default true
+ add lemmas even at regular effort
 
 endmodule

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 0a7ecd14e5d00ea1c0e0ebe011adc26a2cdf2c3e..be2b48f81e86bef01e5d2ac3fea44c889a06de75 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -97,7 +97,7 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
   }
 
-  if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+  if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
     d_external.d_out->lemma(getLemma());
     return;
   }