Solver integration

[brendanzab]

It would be nice to have some static static integer and array bounds checking using some sort of refinement-style thing.

I asked, and granule seems to have some of it in its codebase:

this module deals with compiling our internal theorems into SMT theorems for Z3 to use:

• https://github.com/granule-project/granule/blob/master/frontend/src/Language/Granule/Checker/Constraints.hs
• https://github.com/granule-project/granule/tree/master/frontend/src/Language/Granule/Checker/Constraints

there’s a lot of stuff about doing symbolic representations
the code is in need of some TLC though

[brendanzab]

Z3 or CVC4 might be helpful for this.

[brendanzab]

This looks nifty - checks the witnesses that are returned from SMT solvers: https://github.com/smtcoq/smtcoq (via this twitter thread).