search

usi-verification-and-security / golem

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

Alethe proofs rejected with rule mod_simplify #55

Closed rodrigo7491 closed 9 months ago

rodrigo7491 commented 9 months ago

The alethe proofs for chc-LIA_366 and chc-LIA_379, from CHC-COMP 2023, are being rejected by carcara.

Production command: golem --logic QF_LIA --print-witness --proof-format alethe [file.smt2] Checking command: carcara check --allow-int-real-subtyping --expand-let-bindings [proof.alethe] [file.smt2]

Checking output for chc-LIA_366:

[ERROR] checking failed on step 't77427' with rule 'mod_simplify': expected term '1' to be numerical constant 9.0
invalid

Checking output for chc-LIA_379:

[ERROR] checking failed on step 't6544' with rule 'mod_simplify': expected term '26' to be numerical constant 63.0
invalid
blishko commented 9 months ago

While the issue with modulo has been fixed, it revealed another problem on chc-LIA-Lin_366. I will create a separate issue for that.