Horn logic soundness bug 

Related closed issues: #3811,  #3778
***
```
[635] % z3 small.smt2 
unsat
sat
[636] % 
[636] % cat small.smt2 
(set-option :fp.xform.bit_blast true)
(set-option :fp.xform.scale true)
(assert (forall ((x Int)) (forall ((y Int)) (distinct y x))))
(check-sat)
(check-sat-using horn)
[637] %
```

OS: Ubuntu 18.04
Commit: 6d6881c
