[proof] Fix documentation of array rule (#6770)

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index a42b3077345393947bd5c332382ad1bc8e0a2c5e..c1cf0338afb40247a019620e1cfcea46a5ab7d4f 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -688,9 +688,9 @@ enum class PfRule : uint32_t
   //================================================= Array rules
   // ======== Read over write
   // Children: (P:(not (= i1 i2)))
-  // Arguments: ((select (store a i2 e) i1))
+  // Arguments: ((select (store a i1 e) i2))
   // ----------------------------------------
-  // Conclusion: (= (select (store a i2 e) i1) (select a i1))
+  // Conclusion: (= (select (store a i1 e) i2) (select a i2))
   ARRAYS_READ_OVER_WRITE,
   // ======== Read over write, contrapositive
   // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))