1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index cebf02c9d..ad879d7ab 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -169,9 +169,7 @@ enum class InferenceId
 
   // ---------------------------------- bags theory
   BAGS_NON_NEGATIVE_COUNT,
-  BAGS_MK_BAG_DIFFERENT_ELEMENT,
-  BAGS_MK_BAG_SAME_ELEMENT,
-  BAGS_MK_BAG,
+  BAGS_BAG_MAKE,
   BAGS_EQUALITY,
   BAGS_DISEQUALITY,
   BAGS_EMPTY,
@@ -840,6 +838,15 @@ enum class InferenceId
   // different applications
   //   (not (= (f sk1 .. skn) (g sk1 .. skn))
   UF_HO_MODEL_EXTENSIONALITY,
+  // equivalence of lambda functions
+  //   f = g => forall x. reduce(lambda(f)(x)) = reduce(lambda(g)(x))
+  // This is applied when lamda functions f and g are in the same eq class.
+  UF_HO_LAMBDA_UNIV_EQ,
+  // equivalence of a lambda function and an ordinary function
+  //   f = h => h(t) = reduce(lambda(f)(t))
+  // This is applied when lamda function f and ordinary function h are in the
+  // same eq class.
+  UF_HO_LAMBDA_APP_REDUCE,
   //-------------------- end model-construction specific part
   //-------------------- end HO extension to UF
   //-------------------------------------- end uf theory