From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 21 Jun 2021 14:40:42 +0000 (-0300)
Subject: [proof] Fix documentation of array rule (#6770)
X-Git-Tag: cvc5-1.0.0~1584
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e9491574fe63075a4261c5b385f9b8b0e5e3e9a;p=cvc5.git

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

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index a42b30773..c1cf0338a 100644
--- 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)))