Fix encoding of structs which contain a single struct field

In the case where a struct contains a single struct typed field, then
the construction of the outer class is encoded into the construction of
the inner class which then itself needs to be encoded. Therefore the
result of the encoding itself may need encoding. This general solution
will also avoid further variations on the same issue such as
constructing unions containing structs, or selecting struct fields from
a union etc.

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -203,19 +203,31 @@ exprt struct_encodingt::encode(exprt expr) const
   while(!work_queue.empty())
   {
     exprt &current = *work_queue.front();
-    work_queue.pop();
     // Note that "with" expressions are handled before type encoding in order to
     // facilitate checking that they are applied to structs rather than arrays.
     if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(current))
       if(can_cast_type<struct_tag_typet>(current.type()))
         current = ::encode(*with_expr, ns);
     current.type() = encode(current.type());
+    optionalt<exprt> update;
     if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
-      current = ::encode(*struct_expr);
+      update = ::encode(*struct_expr);
     if(const auto union_expr = expr_try_dynamic_cast<union_exprt>(current))
-      current = ::encode(*union_expr, *boolbv_width);
+      update = ::encode(*union_expr, *boolbv_width);
     if(const auto member_expr = expr_try_dynamic_cast<member_exprt>(current))
-      current = encode_member(*member_expr);
+      update = encode_member(*member_expr);
+    if(update)
+    {
+      INVARIANT(
+        current != *update,
+        "Updates in struct encoding are expected to be a change of state.");
+      current = std::move(*update);
+      // Repeat on the updated node until we reach a fixed point. This is needed
+      // because the encoding of an outer struct/union may be initially
+      // expressed in terms of an inner struct/union which it contains.
+      continue;
+    }
+    work_queue.pop();
     for(auto &operand : current.operands())
       work_queue.push(&operand);
   }

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -169,6 +169,18 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
     const concatenation_exprt expected_result{
       {green_ham.symbol_expr(), forty_two, minus_one}, bv_typet{72}};
     REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
+    SECTION("struct containing a single struct")
+    {
+      const struct_typet struct_struct_type{
+        struct_union_typet::componentst{{"inner", struct_tag}}};
+      const type_symbolt struct_struct_type_symbol{
+        "struct_structt", struct_type, ID_C};
+      test.symbol_table.insert(type_symbol);
+      const struct_tag_typet struct_struct_tag{type_symbol.name};
+      const struct_exprt struct_struct{
+        exprt::operandst{struct_expr}, struct_struct_tag};
+      REQUIRE(test.struct_encoding.encode(struct_struct) == expected_result);
+    }
   }
   SECTION("member expression selecting a data member of a struct")
   {