a: uint; 
b: uint; 
c: uint; 
d: uint; 
// Usually results in a contradiction error 
keep a + 3*b + 12*c + 48*d == 48; 
keep a <= 48; 
keep b <= 16; 
keep c <= 4; 
keep d <= 1;