From 7e9491574fe63075a4261c5b385f9b8b0e5e3e9a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 21 Jun 2021 11:40:42 -0300 Subject: [PATCH] [proof] Fix documentation of array rule (#6770) --- src/proof/proof_rule.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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))) -- 2.30.2