Simplifying Z3 expressions

Question

I am using z3 in Python to simplify some logic expressions and I have question. When I execute the following code

x = BitVec('x', 8)
e = ULT(x - 5, 10)
Then('simplify', 'propagate-values', 'ctx-solver-simplify')(e).as_expr()

I get the result:

Not(ULE(10, 251 + x))

However, this is equivalent to

And(UGE(x, 5), ULT(x, 15))

Is there a way to transform (simplify) the first expression (Not) into the second one (And)? More specifically, is it possible to ask z3 about the ranges of values a specific variable can take (in this example x >= 5 && x < 15)?

Answer 1

You could build a simplifier on top of Z3 by synthesizing the simpler expression among a set of templates. But Z3 does not attempt to perform this particular simplification among many others.