Lower before converting to expression in ::get

In order to fix empty struct support.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -497,14 +497,15 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
     {
       return identifier_descriptor;
     }
-    if(gather_dependent_expressions(expr).empty())
+    const exprt lowered = lower(expr);
+    if(gather_dependent_expressions(lowered).empty())
     {
       INVARIANT(
-        objects_are_already_tracked(expr, object_map),
+        objects_are_already_tracked(lowered, object_map),
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
       return ::convert_expr_to_smt(
-        expr,
+        lowered,
         object_map,
         pointer_sizes_map,
         object_size_function.make_application,

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1044,4 +1044,18 @@ TEST_CASE(
   REQUIRE(test.procedure() == decision_proceduret::resultt::D_SATISFIABLE);
   CHECK(test.sent_commands == expected_check_commands);
   test.sent_commands.clear();
+
+  INFO("Getting values involving empty structs.");
+  test.mock_responses.push_front(
+    smt_get_value_responset{{{expected_handle, smt_bool_literal_termt{true}}}});
+  CHECK(test.procedure.get(equality_expression) == true_exprt{});
+  test.mock_responses.push_front(smt_get_value_responset{
+    {{smt_identifier_termt{"foo", smt_bit_vector_sortt{8}},
+      smt_bit_vector_constant_termt{0, 8}}}});
+  const struct_exprt expected_empty{{}, type_reference};
+  CHECK(test.procedure.get(foo.symbol_expr()) == expected_empty);
+  const std::vector<smt_commandt> expected_get_commands{
+    smt_get_value_commandt{expected_handle},
+    smt_get_value_commandt{expected_foo}};
+  CHECK(test.sent_commands == expected_get_commands);
 }