Add abstraction-refinement for overapporximation via NRA and NIA

[msooseth]

See paper by Hozzova at al. Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification

We could do this as another abstraction-refinement option. May not be too difficult, actually.