This paper proposes an approach to evaluating B formal specifications using constraint logic programming with sets (CLPS). This approach is used to animate and generate test sequences from B formal specifications. The solver, called CLPS–B, is described in terms of constraint domains, consistency verification, and constraint propagation. It is more powerful than most constraint systems because it allows the domain of variable to contain other variables, which increases the level of abstraction. The constrained state propagates the nondeterminism of the B specifications and reduces the number of states in a reachability graph. We illustrate this approach by comparing the constrained state graph exploration with the concrete one in a simple example – process scheduler. We also describe the automated test generation method that uses the CLPS–B solver to better control combinational explosion.