Allow using Eldarica as a backend CHC-solver

hopv / rethfl

ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types

0 stars 0 forks source link

Allow using Eldarica as a backend CHC-solver #1

Closed KenSakayori closed 6 months ago

KenSakayori commented 6 months ago

NB: You cannot test this branch as is because the inlining is broken. I guess we should merge the patch for that bug (and other patches) before merging this branch.

KenSakayori commented 6 months ago

I think --show-refinement should now work for Eldarica, but I'm not quite sure until https://github.com/moratorium08/hflmc2/commit/a4b619584298e795dd9411883a01f3d3ae2451ac and https://github.com/moratorium08/hflmc2/commit/340e556876d88da22fdf716031d71211341e9798 are merged. BTW I might squash the two commits when merging.