Ideas to investigate

I am going to (mis)use issue tracker to keep track of ideas that I would like to investigate.
In no order of priority

- Could buffers keep track of their size?
- In SMTChecker we represent arrays as an ADT consisting of an SMT-LIB Array and a number representing the actual size.
- Does Bitwuzzla support ADTs?
- Could we represent buffers as `(Array Word Word)` instead of `(Array Word Byte)`?
- Can we simplify more on the `Expr` level? Like the common case of reading a previously written value from memory?
- There seems to already be a simplification for [removing irrelevant writes for concrete indices](https://github.com/ethereum/hevm/blob/c873b91fb11d8c420885c9b5fd966d771bea922b/src/EVM/Expr.hs#L571). Could this be generalized to symbolic ones as well (with the help of an SMT solver)?
- What does the test `badvault-sym-branch` actually test?