Audit `smt.py` Z3 translation layer for verification soundness

[aallan]

The vera/smt.py module translates Vera contracts to Z3 assertions. A bug here could cause Z3 to verify a contract as satisfied when it isn't — silently bypassing runtime checks. This is the highest-severity correctness bug class possible in the verifier.

Audit approach:

• For every contract operator translation (arithmetic, comparison, logical), write a test with a known-false contract and verify Z3 rejects it
• Test edge cases: integer overflow, division by zero in contracts, nested quantifiers, contracts referencing @T.result
• Verify that Tier 1 (proved) and Tier 3 (runtime) give the same pass/fail result for the same inputs on a corpus of test functions

This is particularly important because the codebase grew rapidly — soundness gaps could have been introduced during the fast iteration phase.