Revert "Try to keep struct and SMTLIB data types in sync"

This reverts commit 0ba0d32.

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -612,14 +612,21 @@ smt2_convt::parse_struct(const irept &src, const struct_typet &type)
   {
     // Structs look like:
     //  (mk-struct.1 <component0> <component1> ... <componentN>)
-
-    if(src.get_sub().size()!=components.size()+1)
-      return result; // give up
-
+    std::size_t j = 1;
     for(std::size_t i=0; i<components.size(); i++)
     {
       const struct_typet::componentt &c=components[i];
-      result.operands()[i]=parse_rec(src.get_sub()[i+1], c.type());
+      if(is_zero_width(components[i].type(), ns))
+      {
+        result.operands()[i] = nil_exprt{};
+      }
+      else
+      {
+        DATA_INVARIANT(
+          src.get_sub().size() > j, "insufficient number of component values");
+        result.operands()[i] = parse_rec(src.get_sub()[j], c.type());
+        ++j;
+      }
     }
   }
   else
@@ -3218,6 +3225,8 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
     "number of struct components as indicated by the struct type shall be equal"
     "to the number of operands of the struct expression");
 
+  DATA_INVARIANT(!components.empty(), "struct shall have struct components");
+
   if(use_datatypes)
   {
     const std::string &smt_typename = datatype_map.at(struct_type);
@@ -3231,29 +3240,16 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
         it!=components.end();
         it++, i++)
     {
-      if(
-        it->type().id() != ID_struct_tag && it->type().id() != ID_struct &&
-        is_zero_width(it->type(), ns))
-      {
+      if(is_zero_width(it->type(), ns))
         continue;
-      }
-
       out << " ";
       convert_expr(expr.operands()[i]);
     }
 
-    if(components.empty())
-    {
-      out << " ";
-      convert_expr(from_integer(0, unsignedbv_typet{1}));
-    }
-
     out << ")";
   }
   else
   {
-    DATA_INVARIANT(!components.empty(), "struct shall have struct components");
-
     if(components.size()==1)
     {
       const exprt &op = expr.op0();
@@ -4907,6 +4903,9 @@ void smt2_convt::unflatten(
             it!=components.end();
             it++, i++)
         {
+          if(is_zero_width(it->type(), ns))
+            continue;
+
           std::size_t member_width=boolbv_width(it->type());
 
           out << " ";
@@ -4917,12 +4916,6 @@ void smt2_convt::unflatten(
           offset+=member_width;
         }
 
-        if(components.empty())
-        {
-          out << " ";
-          convert_expr(from_integer(0, unsignedbv_typet{1}));
-        }
-
         out << "))"; // mk-, let
       }
     }
@@ -5947,27 +5940,15 @@ void smt2_convt::find_symbols_rec(
 
       for(const auto &component : components)
       {
-        if(
-          component.type().id() != ID_struct_tag &&
-          component.type().id() != ID_struct &&
-          is_zero_width(component.type(), ns))
-        {
+        if(is_zero_width(component.type(), ns))
           continue;
-        }
 
         out << "(" << smt_typename << "." << component.get_name()
                       << " ";
         convert_type(component.type());
         out << ") ";
       }
 
-      if(components.empty())
-      {
-        out << "(" << smt_typename << ".0 ";
-        convert_type(unsignedbv_typet{1});
-        out << ") ";
-      }
-
       out << "))))" << "\n";
 
       // Let's also declare convenience functions to update individual