Add additional assertion to UInt_sqrt

[Gungy2]

Summary

This PR fixes issue #1586 by adding an assertion for the UInt_sqrt function.

[jeapostrophe]

Were you able to test this? Does it make your code work?

[Gungy2]

Yes, it makes my code work. The assertion should only work for the right integer square root, if I am not mistaken.

[Gungy2]

The only issue with this assertion is that, while it is perfect (meaning that it passes just for the exact number) it tends to overwhelm the SMT solver (for my program, which is relatively complex, it times out multiple times). So I am not sure what is the right approach here to strike the balance between correctness (usability) and performance. Alternatively, to get around this, enforce can be used, as pointed out in #1586. If it is decided to not add the assertion, maybe add to the documentation of the functions not covered by the SMT solver that some enforces might be required

[jeapostrophe]

Yea, that matches my priors too. One of the reasons Reach verification can be so fast is that we never use quantification so the theory is really small.