We discuss applications of bit-vector reasoning outside of the HW/SW verification world. 
As an example, we consider a challenge problem in systems biology: A Glass model is a 
restricted system of ODEs, and is frequently used to model biological systems. We 
consider the problem of identifying stable periodic orbits with pre-defined properties. 
We show that combinatorial properties of bit-vectors are at the heart of this problem, 
and discuss various ways of encoding the problem into CNF.