Verified Python
`InferTypesTransformer._handle_overflow()` has some python code to detect when u8 + u8 overflows. Another option is to use z3 prover.

Sample capability:
https://rise4fun.com/Dafny/IFMgr

```
type u8 = x: int | 0 <= x < 255
type u16 = x: int | 0 <= x < 65536

method Add(x: u8, y: u8) returns (r: u8)

{
  r := x+y;
}
```

Roadblocks: The API to z3 is not easy to use. The goal of this task is to extract a minimal z3 script that accomplishes the same thing as the dafny program above.

More context: https://github.com/Z3Prover/z3/discussions/5428, https://github.com/dafny-lang/dafny/issues/1323.
Blog post: https://adsharma.github.io/pysmt/
