Support for SMT-LIB 2.7

[Gbury]

Still WIP, but should be nearly complete.

[Gbury]

With the last commit, all of the new features of SMT-LIB2.7 have been implemented[1]. Once tests pass, I'll probably merge soon.

@bobot depending on how far you are with the why3 printers, would you happen to have a few files that make use of the new features (e.g. polymorphism, higher-order, check-sat-assuming with arbitrary terms) ? That would be helpful to check that the implementation is correct and works as intended.

[1] : though I still have to try and find a sane way to restrict the new functions of the BV theory (i.e. ubv_to_int, sbv_to_int, int_to_bv) to only be present if the Int theory is also present...

[bobot]

I was waiting the merge of this MR for starting the implementation with a reference parser ;) , in any case I will not start before next week.

[Gbury]

Alright, I'll merge this and see if any bug is spotted until the next release.