Golem returns UNSAT for SAT instance

[jena-kling]

Hey, I am working with the latest release of golem and found that it returns the wrong answer for

(set-logic HORN)
(declare-fun pred (Int) Bool )
(assert (forall ((x Int)) (= (pred x) (<= 0 x))))
(check-sat)

That's how I invoke golem:

~/golem -e lawi sat.smt2
unsat

The instance should be sat because a model would be given by (define-fun pred ((A Int)) Bool (>= A 0))

[blishko]

Hi @jena-kling,

Golem often does not work correctly if you go outside the CHC-COMP format. I think I need update the parsing to reject this input. If you split the equivalence into two clauses, it should work correctly.

(set-logic HORN)
(declare-fun pred (Int) Bool )
(assert (forall ((x Int)) (=> (<= 0 x) (pred x))))
(assert (forall ((x Int)) (=> (pred x) (<= 0 x))))
(check-sat)

[blishko]

The problematic input will now be rejected by Golem (see 255f64e1ca085a1dbbe40f1a9d07b400f1135bc7). You'll have to keep individual assertions representable as Horn clauses. I hope that is not a big problem.

Thank you for the report!