SymbolicBitVec has an API that is capable of constructing a completely unique symbolic bit vector using a static atomic counter. However collisions can still occur if values are constructed outside this counter.
A similar API should be exposed by SymbolicBit to construct new variables to prevent collisions, and the direct construction should be avoided. This is somewhat similar to the use of SymbolicBit::And(x, y) being technically possible but discouraged in favor of x & y.
Note that so long as the enum can be accessed, its variants can always be constructed. This could be worked around by having all APIs use a wrapper SymbolicBitValue struct which internally holds a SymbolicBit.