Z3 smt.arith.solver=1 gives incorrect result on incremental LIA formula with just = operator

Hi,
For this formula,
```
(declare-fun a () Int)
(declare-fun b () Int)
(push)
(assert (= b 0))
(check-sat)
(pop)
(assert (= b 0))
(assert (= a 1))
(check-sat)
```
z3 smt.arith.solver=1 incorrectly reports `unsat` to the second `(check-sat)`:
```
% z3 smt.arith.solver=1 small.smt2
sat
unsat
```

OS: Ubuntu 18.04
Revision: 28cb13f