## Invalid multiple solutions with call to isSatisfiable(true) in ModelIterator

I am generating multiple solutions for a sat problem in the following way:

Create the default solver. Call the newVar method with exactly the number of variables in my problem. Call the setExpectedNumberOfClauses method with exactly the number of clauses (not including the added "exactly" constraint). Call addClause multiple times to add all the clauses. Call addExactly to add one "exactly" constraint.

Call isSatisfiable(true) and when this returns true, call model() to get one of the solutions to my problem.

Then, I use addBlockingClause to add the exact opposite of the solution (i.e., negating all the numbers in the solution) to the solver.

I continue by again calling isSatisfiable(true) and if this returns true, call model() to get the next solution to my problem.

I repeat this process until isSatisfiable(true) returns false.

What I am finding is that subsequent calls to isSatisfiable after the first solution is found and I call addBlockingClause to block that solution *do not* respect the "exactly" constraint I have imposed on the solver.

Is this a known problem? Is my strategy for getting multiple solutions sound? Is there a workaround, for example, should I re-assert the exact constraints each time I add a blocking clause?