|
|
|---|
|
|
|
|---|
Use gl to reason about finitely bounded values.
It is often convenient to use as much automation as possible when performing proofs. Gl provides the ability to automatically reason about finite values, such as 32-bit integers. As examples, this can be quite useful when reasoning about cryptography algorithms or verifying hardware.