search

usi-verification-and-security / golem

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

Alethe proof rejected #58

Closed blishko closed 9 months ago

blishko commented 9 months ago

Alethe proof produced by golem is rejected by carcara on chc-LIA-Lin_366. This is another problem on this benchmark revealed after the fix of #55.

Here is the carcara output:

[ERROR] checking failed on step 't145814' with rule 'resolution': pivot was not eliminated: '(main_1 1 2 286 158 9 0)'
invalid
blishko commented 9 months ago

The root cause of the problem was incorrect handling of div operation in proof production and it was fixed in 628838f. The problem was obscured, because older version of carcara also had a bug in handling div operation (see the fix). With latest versions of golem and carcara the produced proof is successfully validated for this benchmark.