Non-refinement variables cause MARVeLus to break

[jlvargasme]

( let x0 : int = 3 )

This does not compile correctly, code create a Z3 null type and cannot be used.