Follow-up work to SMT solver code

runtimeverification / hs-backend-booster

Accelerates K Framework's Haskell backend

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

7 stars 0 forks source link

Closed jberthold closed 9 months ago

jberthold commented 9 months ago

          Follow-up work:

[x] Check ensures clauses with SMT solver
[x] insert comments into the transcript for all declare commands (add a comment field)
[x] extend new SMTOptions type to subsume all we use from the old SMTSolverOptions

Won't do (just yet):

tothtamas28 commented 9 months ago

(I.e. the solver layer has to enable parallel processing of requests.)

ehildenb commented 9 months ago

Also this is related: https://github.com/runtimeverification/haskell-backend/issues/3603 (handling partiality for SMT encoding correctly).