Evaluating a Constraint expression

In reply to dave_59:

Hi Dave ,

Result of Relational Operator is either 1’b0 OR 1’b1 the expression reduces to ::


constraint SIGN_ADDITION { 
                             sum == ( 1'b0 || 1'b1 ) + a + b  ; 
 	                  } 

Due to 1’b0 OR 1’b1 the expression now is treated as Unsigned Expression .

Hence c N d would be Zero-Extended ( instead of Sign-Extended !! )

My question is while deciding the solution space for sum ,
when does the Solver decide to Zero-Extend c N d instead of Sign-Extension ?

Would be first obtain result of ( c < d ) to 1’b0 / 1’b1 and then 0-Extend it ?