go through all examples with z3
single-level records
define functions on our values
generate separate soft equalities for each fields
Revert "generate separate soft equalities for each fields"

This reverts commit ffd27d631fa77020f9b529e558f283f2046d5eee.
fix heap constraints
split example
switch the declaration, makes examples work