Skip to content

Commit

Permalink
fix typo (thanks Bill Mill!)
Browse files Browse the repository at this point in the history
  • Loading branch information
cfbolz committed Jul 13, 2024
1 parent 8171e20 commit 8ff0bc2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion posts/2024/07/finding-simplification-rules-with-z3.md
Original file line number Diff line number Diff line change
Expand Up @@ -336,7 +336,7 @@ int_or(x, x) -> x
## Synthesizing constants

Supporting the next patterns is harder: `op(x, x) == c1`, `op(x, c1) == x`, and
`op(x, c1) == x`. We don't know which constants to pick to try to get Z3 to
`op(c1, x) == x`. We don't know which constants to pick to try to get Z3 to
prove the equality. We could iterate over common constants like `0`, `1`,
`MAXINT`, etc, or even over all the 256 values for a bitvector of length 8.
However, we will instead ask Z3 to find the constants for us too.
Expand Down

0 comments on commit 8ff0bc2

Please sign in to comment.