BoolTactics simplify x to And(True, x)

[zwimer]

When applying BoolTactics to simplify a Bool, the result is not simplified all the way. Specifically, here is my minimal proof of concept:

>>> import z3
>>> c = z3.Context()
>>> x = z3.Bool("x", c)
>>> t = z3.Then(z3.Tactic("simplify", ctx=c),z3.Tactic("propagate-ineqs", ctx=c),z3.Tactic("propagate-values", ctx=c),z3.Tactic("unit-subsume-simplify", ctx=c),z3.Tactic("aig", ctx=c),ctx=c)
>>> print(t(x).as_expr())
And(True, x)

In older versions of z3, such as 4.10, the final line simply printed x as one would expect; the behavior is different in this version 4.12.1.0.

Environment:
Version: 4.12.1.0
A new python virtualenv with pip install z3-solver