Soundness bug in HORN logic

[wintered]

[682] % z3 small.smt2
sat
unsat
[683] % 
[683] % cat small.smt2
(set-option :fp.spacer.gpdr true)
(declare-fun a (Bool Bool Int Int Int Int Int Int Int) Bool)
(assert (forall ((b Int) (bc Bool) (bd Bool) (bk Int) (be Int) (bf Int) (bm Int) (bn Int))
     (=> (= bc bd false) (= bk 0) (a bc bd bf b bm bn bk be b))))
(assert (forall ((bc Bool) (bd Bool) (bf Int) (bm Int) (bn Int) (bk Int) (b Int) (c Int)
         (d Int) (g Int) (e Int) (f Bool) (gn Int) (ge Int) (gl Int) (gd Bool))
     (=> (a bc bd bf b bm bn bk e b) (or (= f bc) (= bk 2)) (a f gd d gl c gn g ge e))))
(assert (forall ((bc Bool) (bd Bool) (bf Int) (bm Int) (bn Int) (bk Int) (be Int) (b Int))
     (=> (a bc bd bf b bm bn bk be b) (or bc bd) false)))
(check-sat-using horn)
(check-sat)
[684] %

OS: Ubuntu 18.04 Commit: 3e9479d