search

usi-verification-and-security / golem

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

Proof length reduction #46

Closed m4mbo closed 11 months ago

m4mbo commented 11 months ago

Changed simplification algorithm from linear cong propagation to a recursive depth-first post order procedure (operation arguments will be simplified before propagating the chain).