Siddharth
Siddharth
CC @hargoniX :)
awaiting-author
awaiting-review
```lean -- @bollu: we need 'hSHA2_k512_length' to allow omega to reason about -- SHA2.k_512.length, which is otherwise treated as an unintepreted constant. have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl...
@alexkeizer comment addressed!
@alexkeizer is this an LGTM from you?
I would love to refactor these tests. That needs us to reach some sort of consensus that we are willing to refactor the test suite for InstCombine. Given such a...
@alexkeizer No, the LLVM evaluation has not been changed by me. What's in the repo is the "latest". I attempted to improve it using `snakemake` here #1549 , but that's...
Ah, thanks for the quick feedback, and the explanation of what's going on! I was trying to reuse `conv` mode, and was trying to use `Tactic.clear` to produce a smaller...
@shilgoel brought this up in conversation today, and I will think a bit on how to add support for this use-case.