Add InferenceIds for theory of arrays (#5910)

This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.

1 files changed, 3 insertions, 2 deletions

diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h
index b4ae228be..96af0b677 100644
--- a/src/theory/arrays/inference_manager.h
+++ b/src/theory/arrays/inference_manager.h
@@ -45,14 +45,15 @@ class InferenceManager : public TheoryInferenceManager
    * @return true if the fact was successfully asserted, and false if the
    * fact was redundant.
    */
-  bool assertInference(TNode atom, bool polarity, TNode reason, PfRule id);
+  bool assertInference(TNode atom, bool polarity, InferenceId id, TNode reason, PfRule pfr);
   /**
    * Send lemma (exp => conc) based on proof rule id with properties p. Cache
    * the lemma if doCache is true.
    */
   bool arrayLemma(Node conc,
+                  InferenceId id,
                   Node exp,
-                  PfRule id,
+                  PfRule pfr,
                   LemmaProperty p = LemmaProperty::NONE,
                   bool doCache = false);