Varbits not handled

Open fruffy opened this issue 6 years ago • 1 comments

It is complicated to support varbits in z3. For now we convert varbit types to bits and evaluate them as such. In the future, we need to add a data structure that will test every possible bit length for varbits.

Oct 10 '19 19:10 fruffy

Possibly relevant work: https://www-cs.stanford.edu/~yoniz/jar20.pdf Hope some form of this gets eventually implemented

Oct 18 '20 20:10 fruffy