From 9d5231dfce32bdc21635a15958f53f8472bfadb6 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 17 May 2023 18:03:15 +0100
Subject: [PATCH 1/8] Add struct encoding class

---
 src/solvers/Makefile                          |  1 +
 .../smt2_incremental/struct_encoding.cpp      | 42 +++++++++
 .../smt2_incremental/struct_encoding.h        | 27 ++++++
 unit/Makefile                                 |  1 +
 .../smt2_incremental/struct_encoding.cpp      | 85 +++++++++++++++++++
 5 files changed, 156 insertions(+)
 create mode 100644 src/solvers/smt2_incremental/struct_encoding.cpp
 create mode 100644 src/solvers/smt2_incremental/struct_encoding.h
 create mode 100644 unit/solvers/smt2_incremental/struct_encoding.cpp

diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index e2d0662981d..0452d9e8319 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -210,6 +210,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
+      smt2_incremental/struct_encoding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \
diff --git a/src/solvers/smt2_incremental/struct_encoding.cpp b/src/solvers/smt2_incremental/struct_encoding.cpp
new file mode 100644
index 00000000000..962e2e9c881
--- /dev/null
+++ b/src/solvers/smt2_incremental/struct_encoding.cpp
@@ -0,0 +1,42 @@
+// Author: Diffblue Ltd.
+
+#include "struct_encoding.h"
+
+#include <util/bitvector_types.h>
+#include <util/make_unique.h>
+
+#include <solvers/flattening/boolbv_width.h>
+
+#include <queue>
+
+struct_encodingt::struct_encodingt(const namespacet &ns)
+  : boolbv_width{util_make_unique<boolbv_widtht>(ns)}
+{
+}
+
+struct_encodingt::struct_encodingt(const struct_encodingt &other)
+  : boolbv_width{util_make_unique<boolbv_widtht>(*other.boolbv_width)}
+{
+}
+
+struct_encodingt::~struct_encodingt() = default;
+
+typet struct_encodingt::encode(typet type) const
+{
+  std::queue<typet *> work_queue;
+  work_queue.push(&type);
+  while(!work_queue.empty())
+  {
+    typet &current = *work_queue.front();
+    work_queue.pop();
+    if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
+    {
+      current = bv_typet{(*boolbv_width)(*struct_tag)};
+    }
+    if(const auto array = type_try_dynamic_cast<array_typet>(current))
+    {
+      work_queue.push(&array->element_type());
+    }
+  }
+  return type;
+}
diff --git a/src/solvers/smt2_incremental/struct_encoding.h b/src/solvers/smt2_incremental/struct_encoding.h
new file mode 100644
index 00000000000..17a1255d957
--- /dev/null
+++ b/src/solvers/smt2_incremental/struct_encoding.h
@@ -0,0 +1,27 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+
+#include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
+
+#include <memory>
+
+class namespacet;
+class boolbv_widtht;
+
+/// Encodes struct types/values into non-struct expressions/types.
+class struct_encodingt final
+{
+public:
+  explicit struct_encodingt(const namespacet &ns);
+  struct_encodingt(const struct_encodingt &other);
+  ~struct_encodingt();
+
+  typet encode(typet type) const;
+
+private:
+  std::unique_ptr<boolbv_widtht> boolbv_width;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
diff --git a/unit/Makefile b/unit/Makefile
index fbe92974ce9..997f2a6cf27 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -114,6 +114,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_object_size.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
+       solvers/smt2_incremental/struct_encoding.cpp \
        solvers/smt2_incremental/theories/smt_array_theory.cpp \
        solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/theories/smt_core_theory.cpp \
diff --git a/unit/solvers/smt2_incremental/struct_encoding.cpp b/unit/solvers/smt2_incremental/struct_encoding.cpp
new file mode 100644
index 00000000000..85114dfb42d
--- /dev/null
+++ b/unit/solvers/smt2_incremental/struct_encoding.cpp
@@ -0,0 +1,85 @@
+// Author: Diffblue Ltd.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <solvers/smt2_incremental/struct_encoding.h>
+#include <testing-utils/use_catch.h>
+
+struct struct_encoding_test_environmentt
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  struct_encodingt struct_encoding{ns};
+
+  static struct_encoding_test_environmentt make()
+  {
+    return {};
+  }
+
+private:
+  struct_encoding_test_environmentt() = default;
+};
+
+TEST_CASE(
+  "struct encoding of non-stuct type is a no-op",
+  "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  typet input = signedbv_typet{8};
+  REQUIRE(test.struct_encoding.encode(input) == input);
+}
+
+TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  REQUIRE(test.struct_encoding.encode(struct_tag) == bv_typet{24});
+}
+
+TEST_CASE("struct encoding of array of structs", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  const auto index_type = signedbv_typet{32};
+  const auto array_size = from_integer(5, index_type);
+  array_typet array_of_struct{struct_tag, array_size};
+  array_typet expected_encoded_array{bv_typet{24}, array_size};
+  REQUIRE(
+    test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
+}
+
+TEST_CASE(
+  "struct encoding of array of array of structs",
+  "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  const auto index_type = signedbv_typet{32};
+  const auto array_size_inner = from_integer(4, index_type);
+  const auto array_size_outer = from_integer(2, index_type);
+  array_typet array_of_struct{struct_tag, array_size_inner};
+  array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
+  array_typet expected_encoded_array{
+    array_typet{bv_typet{24}, array_size_inner}, array_size_outer};
+  REQUIRE(
+    test.struct_encoding.encode(array_of_array_of_struct) ==
+    expected_encoded_array);
+}

From 112da4e015152c5881b17d94a15acc2b6feed522 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 23 May 2023 16:25:36 +0100
Subject: [PATCH 2/8] Refactor to deduplicate unit test setup

As some of the setup is the same for each test, the tests can be
sections in a single test which share the same setup instead of copying
it.
---
 .../smt2_incremental/struct_encoding.cpp      | 69 ++++++++-----------
 1 file changed, 27 insertions(+), 42 deletions(-)

diff --git a/unit/solvers/smt2_incremental/struct_encoding.cpp b/unit/solvers/smt2_incremental/struct_encoding.cpp
index 85114dfb42d..127abe7ed27 100644
--- a/unit/solvers/smt2_incremental/struct_encoding.cpp
+++ b/unit/solvers/smt2_incremental/struct_encoding.cpp
@@ -32,7 +32,7 @@ TEST_CASE(
   REQUIRE(test.struct_encoding.encode(input) == input);
 }
 
-TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
+TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
 {
   const struct_union_typet::componentst components{
     {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
@@ -41,45 +41,30 @@ TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
   auto test = struct_encoding_test_environmentt::make();
   test.symbol_table.insert(type_symbol);
   struct_tag_typet struct_tag{type_symbol.name};
-  REQUIRE(test.struct_encoding.encode(struct_tag) == bv_typet{24});
-}
-
-TEST_CASE("struct encoding of array of structs", "[core][smt2_incremental]")
-{
-  const struct_union_typet::componentst components{
-    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
-  struct_typet struct_type{components};
-  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
-  auto test = struct_encoding_test_environmentt::make();
-  test.symbol_table.insert(type_symbol);
-  struct_tag_typet struct_tag{type_symbol.name};
-  const auto index_type = signedbv_typet{32};
-  const auto array_size = from_integer(5, index_type);
-  array_typet array_of_struct{struct_tag, array_size};
-  array_typet expected_encoded_array{bv_typet{24}, array_size};
-  REQUIRE(
-    test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
-}
-
-TEST_CASE(
-  "struct encoding of array of array of structs",
-  "[core][smt2_incremental]")
-{
-  const struct_union_typet::componentst components{
-    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
-  struct_typet struct_type{components};
-  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
-  auto test = struct_encoding_test_environmentt::make();
-  test.symbol_table.insert(type_symbol);
-  struct_tag_typet struct_tag{type_symbol.name};
-  const auto index_type = signedbv_typet{32};
-  const auto array_size_inner = from_integer(4, index_type);
-  const auto array_size_outer = from_integer(2, index_type);
-  array_typet array_of_struct{struct_tag, array_size_inner};
-  array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
-  array_typet expected_encoded_array{
-    array_typet{bv_typet{24}, array_size_inner}, array_size_outer};
-  REQUIRE(
-    test.struct_encoding.encode(array_of_array_of_struct) ==
-    expected_encoded_array);
+  SECTION("direct struct_tag_type encoding")
+  {
+    REQUIRE(test.struct_encoding.encode(struct_tag) == bv_typet{24});
+  }
+  SECTION("array of structs encoding")
+  {
+    const auto index_type = signedbv_typet{32};
+    const auto array_size = from_integer(5, index_type);
+    array_typet array_of_struct{struct_tag, array_size};
+    array_typet expected_encoded_array{bv_typet{24}, array_size};
+    REQUIRE(
+      test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
+  }
+  SECTION("array of array of structs encoding")
+  {
+    const auto index_type = signedbv_typet{32};
+    const auto array_size_inner = from_integer(4, index_type);
+    const auto array_size_outer = from_integer(2, index_type);
+    array_typet array_of_struct{struct_tag, array_size_inner};
+    array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
+    array_typet expected_encoded_array{
+      array_typet{bv_typet{24}, array_size_inner}, array_size_outer};
+    REQUIRE(
+      test.struct_encoding.encode(array_of_array_of_struct) ==
+      expected_encoded_array);
+  }
 }

From f19227009635a47624981f4f557c21152c88b46c Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 17 May 2023 18:25:27 +0100
Subject: [PATCH 3/8] Add struct encoding support for symbol expressions

---
 .../smt2_incremental/struct_encoding.cpp      | 15 +++++++++++
 .../smt2_incremental/struct_encoding.h        |  2 ++
 .../smt2_incremental/struct_encoding.cpp      | 25 +++++++++++++++++++
 3 files changed, 42 insertions(+)

diff --git a/src/solvers/smt2_incremental/struct_encoding.cpp b/src/solvers/smt2_incremental/struct_encoding.cpp
index 962e2e9c881..e78c2ccd65c 100644
--- a/src/solvers/smt2_incremental/struct_encoding.cpp
+++ b/src/solvers/smt2_incremental/struct_encoding.cpp
@@ -40,3 +40,18 @@ typet struct_encodingt::encode(typet type) const
   }
   return type;
 }
+
+exprt struct_encodingt::encode(exprt expr) const
+{
+  std::queue<exprt *> work_queue;
+  work_queue.push(&expr);
+  while(!work_queue.empty())
+  {
+    exprt &current = *work_queue.front();
+    work_queue.pop();
+    current.type() = encode(current.type());
+    for(auto &operand : current.operands())
+      work_queue.push(&operand);
+  }
+  return expr;
+}
diff --git a/src/solvers/smt2_incremental/struct_encoding.h b/src/solvers/smt2_incremental/struct_encoding.h
index 17a1255d957..b5613012d59 100644
--- a/src/solvers/smt2_incremental/struct_encoding.h
+++ b/src/solvers/smt2_incremental/struct_encoding.h
@@ -3,6 +3,7 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
 
+#include <util/expr.h> // For passing exprt by value. // IWYU pragma: keep
 #include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
 
 #include <memory>
@@ -19,6 +20,7 @@ class struct_encodingt final
   ~struct_encodingt();
 
   typet encode(typet type) const;
+  exprt encode(exprt expr) const;
 
 private:
   std::unique_ptr<boolbv_widtht> boolbv_width;
diff --git a/unit/solvers/smt2_incremental/struct_encoding.cpp b/unit/solvers/smt2_incremental/struct_encoding.cpp
index 127abe7ed27..9449955686d 100644
--- a/unit/solvers/smt2_incremental/struct_encoding.cpp
+++ b/unit/solvers/smt2_incremental/struct_encoding.cpp
@@ -68,3 +68,28 @@ TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
       expected_encoded_array);
   }
 }
+
+TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"green", signedbv_typet{32}}, {"eggs", unsignedbv_typet{16}}};
+  const struct_typet struct_type{components};
+  const type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  const struct_tag_typet struct_tag{type_symbol.name};
+  const symbolt struct_value_symbol{"my_struct", struct_tag, ID_C};
+  test.symbol_table.insert(struct_value_symbol);
+  const auto symbol_expr = struct_value_symbol.symbol_expr();
+  const auto symbol_expr_as_bv = symbol_exprt{"my_struct", bv_typet{48}};
+  SECTION("struct typed symbol expression")
+  {
+    REQUIRE(test.struct_encoding.encode(symbol_expr) == symbol_expr_as_bv);
+  }
+  SECTION("struct equality expression")
+  {
+    const auto struct_equal = equal_exprt{symbol_expr, symbol_expr};
+    const auto bv_equal = equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
+    REQUIRE(test.struct_encoding.encode(struct_equal) == bv_equal);
+  }
+}

From a19b7b301f59ba2f4208ed0f5c2bb84665aba05a Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 17 May 2023 19:47:46 +0100
Subject: [PATCH 4/8] Add encode struct_exprt as field concatenation

---
 src/solvers/smt2_incremental/struct_encoding.cpp |  8 ++++++++
 .../solvers/smt2_incremental/struct_encoding.cpp | 16 ++++++++++++++--
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/solvers/smt2_incremental/struct_encoding.cpp b/src/solvers/smt2_incremental/struct_encoding.cpp
index e78c2ccd65c..f4d3eee040e 100644
--- a/src/solvers/smt2_incremental/struct_encoding.cpp
+++ b/src/solvers/smt2_incremental/struct_encoding.cpp
@@ -2,6 +2,7 @@
 
 #include "struct_encoding.h"
 
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/make_unique.h>
 
@@ -41,6 +42,11 @@ typet struct_encodingt::encode(typet type) const
   return type;
 }
 
+static exprt encode(const struct_exprt &struct_expr)
+{
+  return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
+}
+
 exprt struct_encodingt::encode(exprt expr) const
 {
   std::queue<exprt *> work_queue;
@@ -50,6 +56,8 @@ exprt struct_encodingt::encode(exprt expr) const
     exprt &current = *work_queue.front();
     work_queue.pop();
     current.type() = encode(current.type());
+    if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
+      current = ::encode(*struct_expr);
     for(auto &operand : current.operands())
       work_queue.push(&operand);
   }
diff --git a/unit/solvers/smt2_incremental/struct_encoding.cpp b/unit/solvers/smt2_incremental/struct_encoding.cpp
index 9449955686d..9da96cd2849 100644
--- a/unit/solvers/smt2_incremental/struct_encoding.cpp
+++ b/unit/solvers/smt2_incremental/struct_encoding.cpp
@@ -1,6 +1,7 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -71,9 +72,9 @@ TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
 
 TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
 {
-  const struct_union_typet::componentst components{
+  const struct_union_typet::componentst component_types{
     {"green", signedbv_typet{32}}, {"eggs", unsignedbv_typet{16}}};
-  const struct_typet struct_type{components};
+  const struct_typet struct_type{component_types};
   const type_symbolt type_symbol{"my_structt", struct_type, ID_C};
   auto test = struct_encoding_test_environmentt::make();
   test.symbol_table.insert(type_symbol);
@@ -92,4 +93,15 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
     const auto bv_equal = equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
     REQUIRE(test.struct_encoding.encode(struct_equal) == bv_equal);
   }
+  SECTION("expression for a struct from list of components")
+  {
+    const symbolt green_ham{"ham", signedbv_typet{32}, ID_C};
+    test.symbol_table.insert(green_ham);
+    const auto forty_two = from_integer(42, unsignedbv_typet{16});
+    const exprt::operandst components{green_ham.symbol_expr(), forty_two};
+    const struct_exprt struct_expr{components, struct_tag};
+    const concatenation_exprt expected_result{
+      {green_ham.symbol_expr(), forty_two}, bv_typet{48}};
+    REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
+  }
 }

From c2685f6a8c245002106488b3ec84581398caf863 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 17 May 2023 19:18:18 +0100
Subject: [PATCH 5/8] Refactor smt2 decision procedure to separate lowering

So that multiple lowering transformations can be added and maintained in
a single location in a single order.
---
 .../smt2_incremental_decision_procedure.cpp              | 9 +++++++--
 .../smt2_incremental_decision_procedure.h                | 4 ++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 596e058b8db..28be78f574c 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -268,7 +268,7 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
     return;
   }
 
-  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
+  const exprt lowered_expr = lower(in_expr);
 
   define_dependent_functions(lowered_expr);
   smt_define_function_commandt function{
@@ -514,7 +514,7 @@ void smt2_incremental_decision_proceduret::set_to(
   const exprt &in_expr,
   bool value)
 {
-  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
+  const exprt lowered_expr = lower(in_expr);
   PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n  "
@@ -587,6 +587,11 @@ void smt2_incremental_decision_proceduret::define_object_properties()
   }
 }
 
+exprt smt2_incremental_decision_proceduret::lower(exprt expression)
+{
+  return lower_byte_operators(expression, ns);
+}
+
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index ce46c51029f..ccd721d1fd3 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -93,6 +93,10 @@ class smt2_incremental_decision_proceduret final
   /// Sends the solver the definitions of the object sizes and dynamic memory
   /// statuses.
   void define_object_properties();
+  /// Performs a combination of transformations which reduces the set of
+  /// possible expression forms by expressing these in terms of the remaining
+  /// language features.
+  exprt lower(exprt expression);
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but

From 0b734a290477faec7208d4ae9ea85d740a5616f9 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 30 May 2023 13:26:25 +0100
Subject: [PATCH 6/8] Add struct encoding to incremental smt2 decision
 procedure

So that we have initial struct support in place.
---
 .../smt2_incremental/smt2_incremental_decision_procedure.cpp | 5 +++--
 .../smt2_incremental/smt2_incremental_decision_procedure.h   | 2 ++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 28be78f574c..c04910303e2 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -249,7 +249,8 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     number_of_solver_calls{0},
     solver_process(std::move(_solver_process)),
     log{message_handler},
-    object_map{initial_smt_object_map()}
+    object_map{initial_smt_object_map()},
+    struct_encoding{_ns}
 {
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
@@ -589,7 +590,7 @@ void smt2_incremental_decision_proceduret::define_object_properties()
 
 exprt smt2_incremental_decision_proceduret::lower(exprt expression)
 {
-  return lower_byte_operators(expression, ns);
+  return struct_encoding.encode(lower_byte_operators(expression, ns));
 }
 
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index ccd721d1fd3..ded8f131069 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -13,6 +13,7 @@
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
+#include <solvers/smt2_incremental/struct_encoding.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
 
@@ -169,6 +170,7 @@ class smt2_incremental_decision_proceduret final
   smt_is_dynamic_objectt is_dynamic_object_function;
   /// Precalculated type sizes used for pointer arithmetic.
   type_size_mapt pointer_sizes_map;
+  struct_encodingt struct_encoding;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

From e27f585c37c761a9a16bffe09d2b935374ed004d Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 18 May 2023 19:33:16 +0100
Subject: [PATCH 7/8] Add regression test for simple struct support

---
 regression/cbmc-incr-smt2/structs/simple.c    | 21 +++++++++++++++++++
 regression/cbmc-incr-smt2/structs/simple.desc | 17 +++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/structs/simple.c
 create mode 100644 regression/cbmc-incr-smt2/structs/simple.desc

diff --git a/regression/cbmc-incr-smt2/structs/simple.c b/regression/cbmc-incr-smt2/structs/simple.c
new file mode 100644
index 00000000000..fcff6ace7d2
--- /dev/null
+++ b/regression/cbmc-incr-smt2/structs/simple.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdint.h>
+
+struct my_struct_type
+{
+  int16_t a;
+  int16_t b;
+};
+
+int main()
+{
+  int16_t nondet;
+  struct my_struct_type my_struct;
+  if(nondet == 3)
+    my_struct.a = 10;
+  else
+    my_struct.a = 12;
+  struct my_struct_type struct_copy;
+  struct_copy = my_struct;
+  assert(my_struct.b != 30 || struct_copy.a != 10);
+}
diff --git a/regression/cbmc-incr-smt2/structs/simple.desc b/regression/cbmc-incr-smt2/structs/simple.desc
new file mode 100644
index 00000000000..2d43a25e364
--- /dev/null
+++ b/regression/cbmc-incr-smt2/structs/simple.desc
@@ -0,0 +1,17 @@
+CORE
+simple.c
+--trace
+Passing problem to incremental SMT2 solving
+line 20 assertion my_struct.b != 30 || struct_copy.a != 10: FAILURE
+nondet=3
+struct_copy.a=10
+struct_copy.b=30
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support struct values and traces for a trivial example. At the
+time of adding the regression test, this exercised the conversion code specific
+to struct_tag_typet and struct_exprt. Field sensitivity is expected to eliminate
+many of the struct specific expressions before they can reach the decision
+procedure with this simple example.

From a06d62f0b00556e02cf8748d85bb30379be7a1ba Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 30 May 2023 13:38:43 +0100
Subject: [PATCH 8/8] Show before/after lowering in smt2 decision procedure
 debug output

To make it easier to debug the changes made by lowering operations.
---
 .../smt2_incremental_decision_procedure.cpp        | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index c04910303e2..0f725728aa8 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -515,12 +515,12 @@ void smt2_incremental_decision_proceduret::set_to(
   const exprt &in_expr,
   bool value)
 {
-  const exprt lowered_expr = lower(in_expr);
-  PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n  "
-          << lowered_expr.pretty(2, 0) << messaget::eom;
+          << in_expr.pretty(2, 0) << messaget::eom;
   });
+  const exprt lowered_expr = lower(in_expr);
+  PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
 
   define_dependent_functions(lowered_expr);
   auto converted_term = [&]() -> smt_termt {
@@ -590,7 +590,13 @@ void smt2_incremental_decision_proceduret::define_object_properties()
 
 exprt smt2_incremental_decision_proceduret::lower(exprt expression)
 {
-  return struct_encoding.encode(lower_byte_operators(expression, ns));
+  const exprt lowered =
+    struct_encoding.encode(lower_byte_operators(expression, ns));
+  log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
+    if(lowered != expression)
+      debug << "lowered to -\n  " << lowered.pretty(2, 0) << messaget::eom;
+  });
+  return lowered;
 }
 
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()