search-for-unsound-fstar-and-vampire
Looking for unsoundness when using vampire as a backend for fstar.
As seen in this issue, some encodings can be interpreted as unsound by vampire. This repository tries to look for them in order to discuss if they are soundness issues or z3 black magic.