wrongly unsat result on gurobi

[rubenkindt]

solver: Gurobi
CPMpy: version v0.9.9 commit e79b3af

The file below gives unsat for Gurobi but sat for all other solvers (OR-Tools and MiniZinc's subsolvers). After a small manual review I can say that Gurobi is wrong. Minimizing the input further results in the input to become sat, according to Ignace this could be due to the (probably same) wrong transformation needed to convert the input to Gurobi.

minimalInput.zip

from cpmpy import *

file = "minimalInput" # don't forget to unzip
m = Model().from_file(file)
m.solve(solver="gurobi")
print(m.status())

expected behavior:
Gurobi to give the correct output (it being sat)

bug found while working on my master thesis.

Constraints:
sum([block[3,0], block[3,1], block[3,2], block[3,3], block[3,4], block[3,5], block[3,6]]) == 3
sum([block[4,0], block[4,1], block[4,2], block[4,3], block[4,4], block[4,5], block[4,6]]) == 3
sum([block[5,0], block[5,1], block[5,2], block[5,3], block[5,4], block[5,5], block[5,6]]) == 3
sum([block[6,0], block[6,1], block[6,2], block[6,3], block[6,4], block[6,5], block[6,6]]) == 3
sum([block[0,0], block[1,0], block[2,0], block[3,0], block[4,0], block[5,0], block[6,0]]) == 3
sum([block[0,1], block[1,1], block[2,1], block[3,1], block[4,1], block[5,1], block[6,1]]) == 3
sum([block[0,2], block[1,2], block[2,2], block[3,2], block[4,2], block[5,2], block[6,2]]) == 3
sum([block[0,3], block[1,3], block[2,3], block[3,3], block[4,3], block[5,3], block[6,3]]) == 3
sum([block[0,4], block[1,4], block[2,4], block[3,4], block[4,4], block[5,4], block[6,4]]) == 3
sum([block[0,5], block[1,5], block[2,5], block[3,5], block[4,5], block[5,5], block[6,5]]) == 3
sum([block[0,6], block[1,6], block[2,6], block[3,6], block[4,6], block[5,6], block[6,6]]) == 3
sum([IV0, IV1, IV2, IV3, IV4, IV5, IV6]) == 1
((block[0,0]) * (block[1,0])) == (IV0)
((block[0,1]) * (block[1,1])) == (IV1)
((block[0,2]) * (block[1,2])) == (IV2)
((block[0,3]) * (block[1,3])) == (IV3)
((block[0,4]) * (block[1,4])) == (IV4)
((block[0,5]) * (block[1,5])) == (IV5)
((block[0,6]) * (block[1,6])) == (IV6)

all variables have a int range of [0,1]
edit: the zip file was uploaded twice, removed one;
edit2: manual reviewed the problem to be satisfied, so I'm changing the 'probably wrong' to wrong

[rubenkindt]

The problem is sat under these conditions:
block[0,0] and block[1,0] are 1, making IV0 = 1
all block[0,*] are 0 (* is meant as a wildcard)
all other not yet mentioned block[*,*] are free to sat all the "sum(...) == 3" constraints

[sourdough-bread]

Solver optimisation removed where

(bv[0]) * (bv[1]) == (IV6) 

is transformed to

(bv[0]) + (bv[1]) == (IV6) 

Cannot be changed to and operator, because the transformed expression is not handled by gurobi later on.