horn Soundness bug on QF_LIA formula

Hi,
For this case, Z3  gives an incorrect answer:
```
[746] % z3 small.smt2
sat
unsat
[747] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (or (and a (not b))))
(check-sat)
(check-sat-using horn)
[748] %
```

OS: Ubuntu 18.04
Commit: db9d6d1
