diff options
| -rw-r--r-- | src/theory/sets/inference_manager.cpp | 17 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 5 |
2 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index a2507d6cf..595dd16c3 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -189,15 +189,22 @@ void InferenceManager::split(Node n, int reqPol) } void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess) { - for (const Node& l : lemmas) + if (!d_state.isInConflict()) { - flushLemma(l, preprocess); + for (const Node& l : lemmas) + { + flushLemma(l, preprocess); + } } lemmas.clear(); } void InferenceManager::flushLemma(Node lem, bool preprocess) { + if (d_state.isInConflict()) + { + return; + } if (d_lemmas_produced.find(lem) != d_lemmas_produced.end()) { Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl; @@ -211,11 +218,7 @@ void InferenceManager::flushLemma(Node lem, bool preprocess) void InferenceManager::flushPendingLemmas(bool preprocess) { - for (const Node& l : d_pendingLemmas) - { - flushLemma(l, preprocess); - } - d_pendingLemmas.clear(); + flushLemmas(d_pendingLemmas, preprocess); } bool InferenceManager::hasLemmaCached(Node lem) const diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 30bb4bad0..d6eec3821 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -514,10 +514,7 @@ void TheorySetsPrivate::fullEffortCheck() } // check downwards closure checkDownwardsClosure(); - if (options::setsInferAsLemmas()) - { - d_im.flushPendingLemmas(); - } + d_im.flushPendingLemmas(); if (d_im.hasProcessed()) { continue; |