Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic...

[cvc5.git] / src / theory / strings / inference_manager.cpp

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a8ebd921a548189d4a74ec85b1ce522979921a20..dce038fbf3478902235d3c8ea1f1a3c32a199a0c 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -374,8 +374,12 @@ void InferenceManager::doPendingLemmas()
         d_termReg.registerTermAtomic(n, sks.first);
       }
     }
-
-    d_out.lemma(lem);
+    LemmaProperty p = LemmaProperty::NONE;
+    if (ii.d_id == Inference::REDUCTION)
+    {
+      p |= LemmaProperty::NEEDS_JUSTIFY;
+    }
+    d_out.lemma(lem, p);
   }
   // process the pending require phase calls
   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)