General improvement. Some bugfixes. Overflow protection for multiplication. overflow protection for sum is missing because the Z3 api for it seems to be bugged