Use ASTs in convert_expr

This is in preparation for making convert_expr return an AST.

Author: romainbrenguier

src/solvers/smt2/smt2_conv.cpp

@@ -791,19 +791,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) << '|';
+    print(smt2_astt("|" + convert_identifier(id) + '|'), 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)) << '|';
+    print(
+      smt2_astt("|" + convert_identifier("nondet_" + id2string(id)) + "|"),
+      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;
+    print(smt2_astt(id2string(id)), out);
   }
   else if(expr.id()==ID_typecast)
   {