Verification of modular inverse and square root

[jhoenicke]

This adds a few handwritten benchmarks for modular inverse and square roots.

The status of the files should be correct, unless I made a stupid mistake. Many of the modInv benchmarks cannot be solved by any solver I tested, even the modSimpleTest. It looks like support for modulo in non-linear integer arithmetic is mostly non-existing.

The QF_UFNRA directory contains an automatically generated relaxation, which overapproximates integer division by real division and subtracting an error term. These help to prove unsat for most of the square root benchmarks (yices can handle these), but some benchmarks are sat after the overapproximation.

[hansjoergschurr]

Thank you for the submission.

It seems the check fail now because of the format you chose for the date. It should strictly be of the format yyyyMMdd. So you could rename the files to 20230301-sqrtmodinv-hoenicke/..., 20230328-sqrtmodinv-hoenicke/... , or similar.

[jhoenicke]

I renamed the directories as suggested.

[hansjoergschurr]

I adjusted the header to correspond to the standard headers we have (Generated instead of Written) and merged the branch. I hope this inspires some development on better modulo support.