Parsing or

[naokikob]

I am confused with the way HoIce parses "or".
For the following input, HoIce seems to reject the 2nd and 5th clauses but accepts the other.
(The comments indicates error messages generated by HoIce.)

(set-logic HORN)
(declare-fun X () Bool)
(declare-fun Y () Bool)
(declare-fun Z () Bool)

(assert (forall () (=> (or X Y) Z)))
(assert (forall () (=> (or X (and Y Z)) Z)))  ;; ill-formed horn clause (or, 2)
(assert (forall () (=> (and X (or Y Z)) Z)))
(assert (forall () (=> (and (or X Y) (or X Z)) Z)))
(assert (forall () (=> (and (or X Y) (or X Z) (or X Y)) Z))) ;; error during clause conversion
(check-sat)

[AdrienChampion]

Thank you for the detailed example.

Hoice's parsing and early pre-processing needs some work. It was directed mostly by benchmarks which tend to have a certain shape. I'm really sorry, but this is not something I can fix soon without some help...