Generation of invalid Alethe proof

[annabeks]

Golem (golem test.smt2 --print-witness --proof-format alethe) produces an invalid proof of unsatisfiability for the input:

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (=> true (inv 0)))
(assert (forall ((x Int)) (=> (and (inv x) (= x 0)) false)))
(check-sat)

In the produced proof, step t2 applies to the wrong assumption t1, while it should refer to t0.

(assume t0 (! (=> true (inv 0)) :named @a0))
(assume t1 (! (forall ((x Int)) (=> (and (inv x) (= x 0)) false)) :named @a1))
(step t2 (cl (not (! true :named @LHS0)) (inv 0)) :rule implies :premises (t1))
...

As a result, the proof is invalid: carcara check proof.alethe test.smt2

[ERROR] checking failed on step 't2' with rule 'implies': term '(forall ((x Int)) (=> (and (inv x) (= x 0)) false))' is of the wrong form, expected '(=> phi_1 phi_2)'
invalid

By swapping the input clauses, Golem generates a valid proof.

Golem version: 0.9.0