diff options
| -rw-r--r-- | src/proof/proof_rule.h | 4 |
1 files 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))) |