I have a model counting program bob. On some graph coloring formulas, bob got the right answer only after removing clause learning. That is to say, with clause learning, bob sometimes counts duplicate solutions, while satisfiability remains stable. This would be big news if true.
I don't know precisely how Bob works, but let's talk about clause learning.
Suppose you have a set of variable assignments, $A$, say $x_1 = 0$, $x_2 = 1$, $x_3 = 0$. This is a single clause in disjunctive normal form:
$$A = \neg x_1 \wedge x_2 \wedge \neg x_3$$
The negation of this set of assignments is a single clause in conjunctive normal form:
$$\neg A = x_1 \vee \neg x_2 \vee x_3$$
So if you have a set of variable assignments that you know you never want to see in any solution, you can add its negation to a SAT problem in CNF and it remains a SAT problem in CNF.
With conflict-directed clause learning, you add clauses which correspond to "dead ends" in the search. Suppose you try some assignments and find that this is not a valid SAT solution. This means that you have identified a CNF clause which is unsatisfiable (i.e. a "conflict"). So if you can find an appropriate subset of assignments that inevitably leads to the dead end, and add its negation as a new clause, this has the effect of directing the search so that it will not get stuck in that dead end any more, while also not changing the solution set.
For model counting, you find a solution to the SAT problem, add its negation as a new clause, and then go try to find a solution to the augmented problem.
It would be big news indeed if adding the negation of a known solution to a SAT problem meant that the solution that you explicitly negated is still a solution. I suspect Bob has a bug.