<p>i spent two out of three days chasing down a single bit (i thought the comparison operation has "equal", "not equal", and "less than" flags, but it has "equal", "not equal and not less than", and "less than" flags). since the input to the scrambling function is 128-bit, every time i would feed the execution trace into the SMT solver it would attempt to enumerate every 128-bit integer to prove me wrong, which doesn't work</p>
