In a z3py project, I've noticed that common sub-expressions are not always eliminated.

Simplified example with And(b, c) as common sub-expression:

from z3 import *

a, b, c, d, e = Bools('a b c d e')

solver = Solver()

solver.add(Xor(Xor(And(a, And(b, c)), And(d, And(b, c))), And(e, And(b, c))))

goal = Goal()
goal.add(solver.assertions())
t = Then('simplify', 'bit-blast', 'tseitin-cnf')

cnf = t(goal)[0]

print(cnf)

Output:

[Or(b, k!0),
 Or(c, k!0),
 Or(d, k!0),
 Or(Not(b), Not(c), Not(k!0), Not(d)),
 Or(a, k!1),
 Or(b, k!1),
 Or(c, k!1),
 Or(Not(b), Not(a), Not(c), Not(k!1)),
 Or(b, k!2),
 Or(c, k!2),
 Or(e, k!2),
 Or(Not(b), Not(c), Not(e), Not(k!2)),
 Or(k!0, k!1, k!2, Not(k!3)),
 Or(Not(k!0), Not(k!1), k!2, Not(k!3)),
 Or(Not(k!0), k!1, Not(k!2), Not(k!3)),
 Or(k!0, Not(k!1), Not(k!2), Not(k!3)),
 Or(Not(k!0), Not(k!1), Not(k!2), k!3),
 Or(k!0, k!1, Not(k!2), k!3),
 Or(k!0, Not(k!1), k!2, k!3),
 Or(Not(k!0), k!1, k!2, k!3),
 Not(k!3)]

Rather than generating clauses for And(b, c) just once, three And3() sets of clauses are generated.

Is it possible in z3py, to get common sub-expressions eliminated?