(proof, opt.pb.compile_equality) Longstanding soundness bug on QF_LRA formula

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[676] % z3-4.8.5 proof=true opt.pb.compile_equality=true small.smt2
unsat
[677] % z3-4.8.6 proof=true opt.pb.compile_equality=true small.smt2
unsat
[678] % z3-4.8.7 proof=true opt.pb.compile_equality=true small.smt2
unsat
[679] % z3release proof=true opt.pb.compile_equality=true small.smt2
unsat
[680] % z3release small.smt2
sat
[681] % 
[681] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (<= (+ (ite c 1 0) (ite b 1 0)) 1))
(assert (= (ite c 1 0) (ite (>= (+ (ite b 1 0) (ite a (- 1) 0)) 1) 1 0)))
(assert (<= d 0 (+ (ite b 1 0) (ite a 1 0)) e))
(minimize 0)
(check-sat)
[682] %

OS: Ubuntu 18.04
Commit: f2449df