Spacer returns UNSAT for SAT-instance

[jena-kling]

Hello everyone,

I am currently working with Z3 version 4.13.0 and think that Spacer returns erroneously UNSAT for the following CHC-formula:

( set-logic HORN )
(declare-fun b ( Int ) Bool)
(declare-fun d ( Int ) Bool)

(assert (forall ( ( g Int ) ( l Bool ) ( o Int ) ) (=>  (and (d o)    ( = g ( ite l 1 o ) ))   (d g)))) 
(assert (forall ( ( g Int ) ( l Bool ) ) (=> ( = g ( ite l 1 0 ) )  (d g))))
(assert (forall ( ( l Int )) (=>  (>= l 1) (b (+ l 1))))) 
(assert (forall ( ( g Int )  ( l Bool ) ) (=> (d g) (b g))))  
(assert (=>  (b (- 1)) (b 0)))
(assert  (=>  (b (- 1)) false))
(check-sat)

$ z3 sat.smt2
unsat

A model for the CHC system would be given by

(define-fun d ((x!0 Int)) Bool
  (> x!0 (- 1)))
(define-fun b ((x!0 Int)) Bool
  (> x!0 (- 1)))

[NikolajBjorner]

it would be slicing. Workaround: fp.xform.slice=false