Counter-Examples & Model Extraction

When a contract is violated, SemanticVerifier.ModelParser parses the S-expression output of Z3 (get-model) into structured Elixir constants and function terms.