search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

Alethe: Generalize proof building to support non-normalized input #62

Closed blishko closed 5 months ago

blishko commented 5 months ago

This PR simplifies the proof building code and generalizes it to handle also non-normalized input, i.e., input where not all predicate arguments are variables.

Detailed description of the changes are in the separate commit messages.