Pretty-printing of multi-variable let expressions

Fix expr2c and format to support LET expressions over multiple
variables. expr2c in fact wouldn't even correctly support
single-variable LET expressions anymore as it wasn't updated in
71a20e9.

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -924,18 +924,24 @@ std::string expr2ct::convert_let(
   const let_exprt &src,
   unsigned precedence)
 {
-  if(src.operands().size()<3)
-    return convert_norep(src, precedence);
+  std::string dest = "LET ";
 
-  unsigned p0;
-  std::string op0=convert_with_precedence(src.op0(), p0);
+  bool first = true;
 
-  std::string dest="LET ";
-  dest+=convert(src.symbol());
-  dest+='=';
-  dest+=convert(src.value());
-  dest+=" IN ";
-  dest+=convert(src.where());
+  const auto &values = src.values();
+  auto values_it = values.begin();
+  for(auto &v : src.variables())
+  {
+    if(first)
+      first = false;
+    else
+      dest += ", ";
+
+    dest += convert(v) + "=" + convert(*values_it);
+    ++values_it;
+  }
+
+  dest += " IN " + convert(src.where());
 
   return dest;
 }

src/util/format_expr.cpp

@@ -369,9 +369,26 @@ void format_expr_configt::setup()
   };
 
   expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
-    return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
-              << format(to_let_expr(expr).value()) << " IN "
-              << format(to_let_expr(expr).where());
+    const auto &let_expr = to_let_expr(expr);
+
+    os << "LET ";
+
+    bool first = true;
+
+    const auto &values = let_expr.values();
+    auto values_it = values.begin();
+    for(auto &v : let_expr.variables())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(v) << " = " << format(*values_it);
+      ++values_it;
+    }
+
+    return os << " IN " << format(let_expr.where());
   };
 
   expr_map[ID_lambda] =