Support for saturating arithmetic is not yet implemented in incremental smt2 decision procedure. This causes a failure with invariant in dispatch_expr_to_smt_conversion about unknown kind saturating_minus as an example. This is required for the following test - cbmc/saturating_arithmetric/test.desc