The design of the language is done in a manner that allows us to translate the code (and all conditions) into very friendly SMTLib code -- that we don't need to add a lot of additional checks like frame rules or havocs and where the set of theories (and their combinations) are well behaved.

We have some info on this in the research papers section and documents but are planning on a full paper focused on how this is done (particularly in the presence of union types, dynamic records/tuples, etc.)