From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 24 Jun 2014 16:15:42 +0000 (-0400)
Subject: fix sets eager lemmas
X-Git-Tag: cvc5-1.0.0~6712^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c57e0640f56ce5286870f27c9f1a9af6dd7e757f;p=cvc5.git

fix sets eager lemmas
---

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;
   }