Add Certora verification for `abs` and `safeAbs`

[QGarchery]

Issues:

• CVL1 throws an error when taking the negation of a mathint
• CVL2 does not allow to use big constants with bit vector encoding

Since we migrated to CVL2, the solution chosen is to only use the bitvector encoding when needed