500ms per one call, we'll make it configurable later.

So that the tests will not run indefinitely.

We must unify the variables in path conditions.

We must pop on all paths from the safe solver.
We did not pop when we failed getting the decomposed literal.

Fix the case when the diff is negative.

So that we got the literal with right variables.

We just return the new value with different type as the python
int is signed. Also, assert that the given value is int.