z3: boolvar-sum with int error

[tias]

a bit artificial, but it exists in bigtest

bv = boolvar(3)
a = [bv[0], 0, bv[2]]
Model(sum(a) > 0).solve("z3")

weirdly, the wsum version does work

bv = boolvar(3)
a = [2*bv[0], 0, 5*bv[2]]
Model(sum(a) > 0).solve("z3")

[IgnaceBleukx]

It seems z3 really does not like integer arithmetic mixed with boolean variables... Just making a sum with integer variables and constants does work weirdly.
I will open an issue on their github page and check if they can/want to fix it on their side or we should use the same "if-then-else" trick as we have done in z3 many times before...

[Dimosts]

this issue is also linked to the one @Wout4 mentions in the comments of #146. Just an "a & 1" constraint crashes the solver due to 1 being an integer.

[IgnaceBleukx]

Yes it is certainly related, although I would expect Sum to work with mixed types...
Got response from the maintainers of z3: Z3Prover/z3#6598
I actually was not aware of the IntVal and BoolVal constructs, we might be able to simplify quite a lot of type-fixing we have at the moment with it.