<p>instead of: QF_BVA</p><p>have you considered: QF_BV and you concatenate all of your symbolic RAM into one big bit vector you shift by your load address</p><p>this will probably be faster and work on more solvers</p>