I fail to prove that equivalent structures equal.
For example: init.c init.smt2
(There are other example with initialization but I think that this one captures all what we use)