diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-21 11:40:42 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-21 14:40:42 +0000 |
| commit | 7e9491574fe63075a4261c5b385f9b8b0e5e3e9a (patch) | |
| tree | 7b0776b9c1f343e9d177a2a6ef2ac0edc37405fb | |
| parent | 5e6117cc183513bf676b36078e6507b31caa6ff0 (diff) | |
[proof] Fix documentation of array rule (#6770)
| -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))) |