`symbolic`: Use new Crucible goal-proving helpers - Githubissues

GaloisInc / macaw

Open source binary analysis tools.

BSD 3-Clause "New" or "Revised" License

203 stars 20 forks source link

`symbolic`: Use new Crucible goal-proving helpers #391

Closed langston-barrett closed 2 months ago

langston-barrett commented 3 months ago

Soon, Crucible will have a new API for dispatching proof obligations. Uses of that API could replace the following code in macaw-symbolic:

https://github.com/GaloisInc/macaw/blob/645754178a034c22e97aac49a962c99b387aaa01/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L318-L352