This directory contains a circuit for the computation of the so-called
3n+1 numbers. The CTL formula checks that all trajectories that do not
overflow end up in the cycle 4-2-1.

This model uses 26-bit numbers and model checking takes substantial time
(about 3 hours on a 200MHz P6).