<p>if SMT-LIB was designed for actually useful applications it would have had a function to replace a chunk of a bitvector with something else, instead of forcing you to do a {let binder, extract, extract, concat} dance and hope whatever you're using to emit code is flexible enough that you can actually get the let binder to work (or you end up with quadratic growth of SMT-LIB terms)</p>
