$ z3 model_validate=true bug.smt2
failed to verify: (let ((a!1 (or (not a) (not c) (not (= a (ite b c a))))))
  (= (and c a) a!1))
evaluated to false
(params keep_cardinality_constraints true pb.solver solver)
mc0
a |-> 1
c |-> 2
$ cat bug.smt2
(declare-fun a () Bool) 
(declare-fun b () Bool) 
(declare-fun c () Bool) 
(assert (= (not (ite c a false)) 
(= 0 (=> (= a (ite  b  c a)) c a false)))) 
(check-sat)