Export correctness witnesses (invariants)
AVR exports the inductive invariant it finds in VMT format (an extension of SMT-LIB 2). We should investigate how to translate it back to the C program level and export it in a standardized exchangeable witness format.