Use ASTs in convert_expr

This is in preparation for making convert_expr return an AST.

Author: romainbrenguier

src/solvers/smt2/smt2_conv.cpp

@@ -880,19 +880,21 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     const irep_idt &id = to_symbol_expr(expr).get_identifier();
     DATA_INVARIANT(!id.empty(), "symbol must have identifier");
-    out << '|' << convert_identifier(id) << '|';
+    smt2_ast_symbolt::make(
+      "|" + convert_identifier(id) + '|')->print(out);
   }
   else if(expr.id()==ID_nondet_symbol)
   {
     const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();
     DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
-    out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
+    smt2_ast_symbolt::make(
+      "|" + convert_identifier("nondet_"+id2string(id)) + "|")->print(out);
   }
   else if(expr.id()==ID_smt2_symbol)
   {
     const irep_idt &id = to_smt2_symbol(expr).get_identifier();
     DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier");
-    out << id;
+    smt2_ast_symbolt::make(id2string(id))->print(out);
   }
   else if(expr.id()==ID_typecast)
   {