larger example

Let's create a large example of some algorithm, which contains `div` somewhere deep inside. Let's make sure we find a bug in it. Let's intentionally make SMT expressions large enough to check how it all works.