1 files changed, 9 insertions, 0 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 87e8565ca..e7464dd24 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -163,6 +163,15 @@ enum class PfRule : uint32_t
   // Notice that we apply rewriting on the witness form of F and G, similar to
   // MACRO_SR_PRED_INTRO.
   MACRO_SR_PRED_TRANSFORM,
+  // ======== Theory Rewrite
+  // Children: none
+  // Arguments: (t, preRewrite?)
+  // ----------------------------------------
+  // Conclusion: (= t t')
+  // where
+  //  t' is the result of applying either a pre-rewrite or a post-rewrite step
+  //  to t (depending on the second argument).
+  THEORY_REWRITE,
 
   //================================================= Processing rules
   // ======== Preprocess