diff options
| -rw-r--r-- | src/theory/datatypes/inference.cpp | 4 | ||||
| -rw-r--r-- | src/theory/datatypes/inference_manager.cpp | 5 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp index 5d68159f7..d03bb0f2f 100644 --- a/src/theory/datatypes/inference.cpp +++ b/src/theory/datatypes/inference.cpp @@ -65,8 +65,8 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma) { // Check to see if we have to communicate it to the rest of the system. // The flag asLemma is true when the inference was marked that it must be - // sent as a lemma in addPendingInference below. - if (asLemma || mustCommunicateFact(d_conc, d_exp)) + // sent as a lemma. + if (asLemma) { return d_im->processDtLemma(d_conc, d_exp, getId()); } diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index affa401d4..496881a33 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -58,7 +58,10 @@ void InferenceManager::addPendingInference(Node conc, bool forceLemma, InferenceId i) { - if (forceLemma) + // if we are forcing the inference to be processed as a lemma, or if the + // inference must be sent as a lemma based on the policy in + // mustCommunicateFact. + if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp)) { d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, i)); } |