shingarov / MachineArithmetic

A mathematical foundation for Smalltalk-25
MIT License
17 stars 6 forks source link

[Z3] Add GaussBvTestTest #248

Closed shingarov closed 6 months ago

shingarov commented 6 months ago

Anticipating Gauss test in Sprite, we build an intuition for why we should expect BV overflows to not affect the validity of the proof.

(Note the "TestTest" in the class name, symbolizing that we are just testing, not proving).