637d8b2a2d
This PR adds SMT-LIB operators to detect overflow `BitVec.negOverflow`, according to the [SMTLIB standard](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2), and the theorem proving equivalence of such definition with the `BitVec` library functions (`negOverflow_eq`). Co-authored by @bollu and @alexkeizer --------- Co-authored-by: Siddharth <siddu.druid@gmail.com> |
||
|---|---|---|
| .. | ||
| Classes | ||
| Data | ||
| Internal | ||
| Net | ||
| Sat | ||
| Sync | ||
| Tactic | ||
| Time | ||
| Classes.lean | ||
| Data.lean | ||
| Internal.lean | ||
| Net.lean | ||
| Sat.lean | ||
| Sync.lean | ||
| Tactic.lean | ||
| Time.lean | ||