fix sets eager lemmas

2 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/sets/options b/src/theory/sets/options
index dc6c6e907..1c95e78e4 100644
--- 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 0a7ecd14e..be2b48f81 100644
--- 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;
   }