Make convert_expr return AST

This allows to separate the creation of the structure of the AST from
its printing.
Unfortunately all the functions we modify here are mutualy recursive so
they have to be modified all at once. That's why this commit is so big.

The correctness of this change is checked by the regression test that
are run using:
scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
which is done by travis.

Author: romainbrenguier