Arthmetic constraints in eclipse

Hello!

I am performing a study into arithmetic constraints in CSPs and the best 
ways of representing them, so would like to be sure I know what eclipse 
currently does.

It appears to me that eclipse will multiply out all brackets and then take 
any terms from the resulting expression with more than one CSP variable in 
them and move them into a new expression, even if this is less efficient 
than taking the original statement given and factoring that into multiple 
expressions... ie solver would go:
(A+1)(B+1)=0 to
AB+A+B+1=0 to
AB=C, C+A+B+1=0

rather than:
(A+1)(B+1)=0
C=A+1,D=B+1,CD=0.


In all cases.. is this correct?

Also what kind of pruning will solver do on the terms of the type "ABC=D" 
that it generates in this way?

I apologize if this is in the documentation but I was unable to find it and 
wished to be sure I was correct.

Chris