Bug multiple sat/1 combined with weighted_maximum/3

Should weighted_maximum/3 work together with multiple sat/1
constraints. I get the following result:

/* SWI-Prolog (threaded, 64 bits, version 8.3.20) */
̀?- sat(~(Y*X)), sat(Z=:=Y), weighted_maximum([7,2,5],[X,Y,Z],W).
false.

But was rather expecting:

?- sat(~(Y*X)), sat(Z=:=Y), weighted_maximum([7,2,5],[X,Y,Z],W).
Y = 1, X = 0, Z = 1, W = 7 ;
Y = 0, X = 1, Z = 0, W = 7