Solving arithmetic constraints using SMT solvers

[jad-hamza]

Add a rule for solving integer arithmetic constraints using Z3 and CVC4 binaries.

The current files (commented out) are:

• https://github.com/epfl-lara/StainlessFit/blob/0b019e5210cbe66c746e9919eec4770fa1608195/core/src/main/scala/smt/SMTInterface.scala
• https://github.com/epfl-lara/StainlessFit/blob/0b019e5210cbe66c746e9919eec4770fa1608195/core/src/main/scala/typechecker/TypeCheckerSMTRules.scala

The current code uses scalaz3 instead of Z3 and CVC4 binaries. Moreover, we need to make sure we translate natural numbers and their corresponding operations (in particular subtraction) properly to match the semantics of our language.