Mysterious bug around conditional branching

[shiatsumat]

The following CHC system is satisfiable (which CHC solvers like Spacer rightly judge), but hoice (ver.1.8.3) judges it unsatisfiable. Probably this bug is related to conditional branching.

(set-logic HORN)

(declare-fun main (Bool) Bool)
(declare-fun go (Int Int Bool) Bool)
(declare-fun go2 (Int Bool) Bool)

(assert (forall ((r Bool)) (=> (go 0 0 r) (main r))))
(assert (forall ((r Bool)) (=> (go 1 1 r) (main r))))
(assert (forall ((n Int)) (go n 0 true)))
(assert (forall ((n Int) (m Int) (r Bool))
  (=> (and (distinct m 0) (go2 n r)) (go n m r))))
(assert (forall ((? Int)) (go2 1 true)))
(assert (forall ((n Int)) (=> (distinct n 1) (go2 n false))))

(assert (forall ((r Bool)) (=> (main r) r)))
(check-sat)

[AdrienChampion]

Thank you for the bug report!

Hoice solves this CHC instance by pre-processing:

❯ hoice -v test.smt2
; Running top pre-processing
; unsat
; solved by pre-processing
unsat

I'm trying to compare with Spacer, but unfortunately the model it returns (with Z3 4.8.8) does not work:

❯ z3 fp.engine=spacer model_validate=true test.smt2
sat
(model
  (define-fun main ((x!0 Bool)) Bool
    true)
  (define-fun go2 ((x!0 Int) (x!1 Bool)) Bool
    (or (and (= x!0 1) x!1) (and (not (= x!0 1)) (not x!1))))
  (define-fun go ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
    (or (and (= x!1 0) x!2) (not x!2) (and (= x!0 1) x!2)))
)

The definition for main does not respect the last clause, it is not true that ∀ r: Bool, true ⇒ r.

Are you positive these clauses are satisfiable? If you are, can you produce a (correct) model for these clauses?

[shiatsumat]

It seems that a bug of Spacer was also found 😄

The following is a solution to the CHC system.

main r <=> r = true
go n m r <=> r = (m = 0 || n = 1)
go2 n r <=> r = (n = 1)