Ideas to investigate

[blishko]

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. 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?