Debug branch: Soundness bug on BV+LIA formula

Hi,
For this formula:
```
(declare-fun a () Int)
(assert (= (div 1 a 2) (bv2nat ((_ int2bv 7) a))))
(check-sat)
```
Z3 debug branch  gives an incorrect answer:
```
[740] % z3 small.smt2 
sat
[741] % z3debug small.smt2 
unsat
[742] % 
[742] % cat small.smt2 
(declare-fun a () Int)
(assert (= (div 1 a 2) (bv2nat ((_ int2bv 7) a))))
(check-sat)
```

OS: Ubuntu 18.04
Commit: 8d39694
