Add all QF_BV builtins - Githubissues

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

94 stars 19 forks source link

Add all QF_BV builtins #41

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

Currently the BitVec translation only knows about FixedSizeBitVectors symbols, but we should have everything including defined symbols specified in QF_BV.