z3.Tactics returning z3.unknown upon BitVecRef < BitVecRef

[Notselwyn]

Hi, the following returns z3.unknown on PIP package z3-solver ver 4.13.0.0:

s = z3.Then('elim-term-ite', 'solve-eqs').solver()
s.add(z3.BitVec("abc", 12) > z3.BitVecVal(0x200, 12))
s.check()  # z3.unknown

s.reason_unknown() returns "unknown". It is not specific to elim-term-ite or solve-eqs.

I'm confident this is a bug, because the following examples do return z3.sat:

z3.solve(z3.BitVec("abc", 12) > z3.BitVecVal(0x200, 12))

s = z3.Solver()
s.add(z3.BitVec("abc", 12) > z3.BitVecVal(0x200, 12))
s.check()

The same happens for <, >, <=, etc

[NikolajBjorner]

try

s = z3.Then('elim-term-ite', 'solve-eqs', 'smt').solver()

otehrwise it will only run the two tactics that you specify and they are not complete solvers.

[Notselwyn]

Great, thanks!