(smt.ematching=false) Soundness bug with declare-datatypes

[muchang]

Hi,
For this case, Z3 smt.ematching=false gives an incorrect answer:

[650] % z3 small.smt2
unsat
[651] % z3 smt.ematching=false small.smt2
sat
[652] % 
[652] % cat small.smt2
(declare-datatypes ((a 0)) (((b (c a)) d)))
(declare-sort i)
(declare-fun e (i) a)
(assert (forall ((f i)) (ite ((_ is d) (e f)) true (ite ((_ is b) (e f)) (forall ((g i)) (= (e g) (c (e f)))) true))))
(assert (exists ((h a) (g i)) (= (e g) h)))
(check-sat)
[653] %

OS: Ubuntu 18.04
Commit: 164a73f

[NikolajBjorner]

regression from b8c069c