From 35a9619862e5b08bdfcb43b14c28d67424bcf88d Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Mon, 18 Jul 2022 18:12:33 +0100
Subject: [PATCH 01/11] Add identifier table parameter to response validation

So that the sort of identifiers can be used for further validation.
---
 .../smt2_incremental_decision_procedure.cpp   | 16 +++--
 .../smt2_incremental_decision_procedure.h     |  1 +
 .../smt_response_validation.cpp               |  4 +-
 .../smt_response_validation.h                 |  5 +-
 .../smt2_incremental/smt_solver_process.cpp   |  6 +-
 .../smt2_incremental/smt_solver_process.h     |  8 ++-
 .../smt2_incremental_decision_procedure.cpp   |  4 +-
 .../smt_response_validation.cpp               | 64 +++++++++++--------
 8 files changed, 65 insertions(+), 43 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 4d6a1241a58..c8ce014e30a 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -27,12 +27,13 @@
 /// return a success status followed by the actual response of interest.
 static smt_responset get_response_to_command(
   smt_base_solver_processt &solver_process,
-  const smt_commandt &command)
+  const smt_commandt &command,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   solver_process.send(command);
-  auto response = solver_process.receive_response();
+  auto response = solver_process.receive_response(identifier_table);
   if(response.cast<smt_success_responset>())
-    return solver_process.receive_response();
+    return solver_process.receive_response(identifier_table);
   else
     return response;
 }
@@ -317,6 +318,7 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   });
   optionalt<smt_termt> descriptor =
     get_identifier(expr, expression_handle_identifiers, expression_identifiers);
+
   if(!descriptor)
   {
     if(gather_dependent_expressions(expr).empty())
@@ -350,8 +352,8 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
     }
   }
   const smt_get_value_commandt get_value_command{*descriptor};
-  const smt_responset response =
-    get_response_to_command(*solver_process, get_value_command);
+  const smt_responset response = get_response_to_command(
+    *solver_process, get_value_command, identifier_table);
   const auto get_value_response = response.cast<smt_get_value_responset>();
   if(!get_value_response)
   {
@@ -464,8 +466,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
   define_object_sizes();
-  const smt_responset result =
-    get_response_to_command(*solver_process, smt_check_sat_commandt{});
+  const smt_responset result = get_response_to_command(
+    *solver_process, smt_check_sat_commandt{}, identifier_table);
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
   {
     if(check_sat_response->kind().cast<smt_unknown_responset>())
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index f89fee0b8ab..e951196fc30 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -131,6 +131,7 @@ class smt2_incremental_decision_proceduret final
   /// array expressions when support for them is implemented.
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_identifiers;
+  std::unordered_map<irep_idt, smt_identifier_termt> identifier_table;
   /// This map is used to track object related state. See documentation in
   /// object_tracking.h for details.
   smt_object_mapt object_map;
diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
index 9634eb79339..941b789bcf2 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -353,7 +353,9 @@ valid_smt_get_value_response(const irept &parse_tree)
   }
 }
 
-response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
+response_or_errort<smt_responset> validate_smt_response(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   if(parse_tree.id() == "sat")
     return response_or_errort<smt_responset>{
diff --git a/src/solvers/smt2_incremental/smt_response_validation.h b/src/solvers/smt2_incremental/smt_response_validation.h
index 81b3d8f411b..c98b0f2cd72 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.h
+++ b/src/solvers/smt2_incremental/smt_response_validation.h
@@ -38,7 +38,8 @@ class response_or_errort final
   std::vector<std::string> messages;
 };
 
-NODISCARD response_or_errort<smt_responset>
-validate_smt_response(const irept &parse_tree);
+NODISCARD response_or_errort<smt_responset> validate_smt_response(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
diff --git a/src/solvers/smt2_incremental/smt_solver_process.cpp b/src/solvers/smt2_incremental/smt_solver_process.cpp
index 1b0079ac33e..9039341653e 100644
--- a/src/solvers/smt2_incremental/smt_solver_process.cpp
+++ b/src/solvers/smt2_incremental/smt_solver_process.cpp
@@ -53,7 +53,8 @@ static void handle_invalid_smt(
   throw analysis_exceptiont{"Invalid SMT response received from solver."};
 }
 
-smt_responset smt_piped_solver_processt::receive_response()
+smt_responset smt_piped_solver_processt::receive_response(
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   const auto response_text = process.wait_receive();
   log.debug() << "Solver response - " << response_text << messaget::eom;
@@ -61,7 +62,8 @@ smt_responset smt_piped_solver_processt::receive_response()
   const auto parse_tree = smt2irep(response_stream, log.get_message_handler());
   if(!parse_tree)
     throw deserialization_exceptiont{"Incomplete SMT response."};
-  const auto validation_result = validate_smt_response(*parse_tree);
+  const auto validation_result =
+    validate_smt_response(*parse_tree, identifier_table);
   if(const auto validation_errors = validation_result.get_if_error())
     handle_invalid_smt(*validation_errors, log);
   return *validation_result.get_if_valid();
diff --git a/src/solvers/smt2_incremental/smt_solver_process.h b/src/solvers/smt2_incremental/smt_solver_process.h
index 3c174b486b0..0b677688228 100644
--- a/src/solvers/smt2_incremental/smt_solver_process.h
+++ b/src/solvers/smt2_incremental/smt_solver_process.h
@@ -21,7 +21,9 @@ class smt_base_solver_processt
   ///    solver process.
   virtual void send(const smt_commandt &command) = 0;
 
-  virtual smt_responset receive_response() = 0;
+  virtual smt_responset
+  receive_response(const std::unordered_map<irep_idt, smt_identifier_termt>
+                     &identifier_table) = 0;
 
   virtual ~smt_base_solver_processt() = default;
 };
@@ -41,7 +43,9 @@ class smt_piped_solver_processt : public smt_base_solver_processt
 
   void send(const smt_commandt &smt_command) override;
 
-  smt_responset receive_response() override;
+  smt_responset receive_response(
+    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+    override;
 
   ~smt_piped_solver_processt() override = default;
 
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index a5e5c564edc..95d4b598f67 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -81,7 +81,9 @@ class smt_mock_solver_processt : public smt_base_solver_processt
     _send(smt_command);
   }
 
-  smt_responset receive_response() override
+  smt_responset receive_response(
+    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+    override
   {
     return _receive();
   }
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
index 0892b31ed07..6eb674f7ce1 100644
--- a/unit/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -35,27 +35,27 @@ TEST_CASE("response_or_errort storage", "[core][smt2_incremental]")
 TEST_CASE("Validation of check-sat repsonses", "[core][smt2_incremental]")
 {
   CHECK(
-    *validate_smt_response(*smt2irep("sat").parsed_output).get_if_valid() ==
+    *validate_smt_response(*smt2irep("sat").parsed_output, {}).get_if_valid() ==
     smt_check_sat_responset{smt_sat_responset{}});
   CHECK(
-    *validate_smt_response(*smt2irep("unsat").parsed_output).get_if_valid() ==
-    smt_check_sat_responset{smt_unsat_responset{}});
+    *validate_smt_response(*smt2irep("unsat").parsed_output, {})
+       .get_if_valid() == smt_check_sat_responset{smt_unsat_responset{}});
   CHECK(
-    *validate_smt_response(*smt2irep("unknown").parsed_output).get_if_valid() ==
-    smt_check_sat_responset{smt_unknown_responset{}});
+    *validate_smt_response(*smt2irep("unknown").parsed_output, {})
+       .get_if_valid() == smt_check_sat_responset{smt_unknown_responset{}});
 }
 
 TEST_CASE("Validation of SMT success response", "[core][smt2_incremental]")
 {
   CHECK(
-    *validate_smt_response(*smt2irep("success").parsed_output).get_if_valid() ==
-    smt_success_responset{});
+    *validate_smt_response(*smt2irep("success").parsed_output, {})
+       .get_if_valid() == smt_success_responset{});
 }
 
 TEST_CASE("Validation of SMT unsupported response", "[core][smt2_incremental]")
 {
   CHECK(
-    *validate_smt_response(*smt2irep("unsupported").parsed_output)
+    *validate_smt_response(*smt2irep("unsupported").parsed_output, {})
        .get_if_valid() == smt_unsupported_responset{});
 }
 
@@ -66,12 +66,13 @@ TEST_CASE(
   SECTION("Parse tree produced is not a valid SMT-LIB version 2.6 response")
   {
     const response_or_errort<smt_responset> validation_response =
-      validate_smt_response(*smt2irep("foobar").parsed_output);
+      validate_smt_response(*smt2irep("foobar").parsed_output, {});
     CHECK(
       *validation_response.get_if_error() ==
       std::vector<std::string>{"Invalid SMT response \"foobar\""});
     CHECK(
-      *validate_smt_response(*smt2irep("()").parsed_output).get_if_error() ==
+      *validate_smt_response(*smt2irep("()").parsed_output, {})
+         .get_if_error() ==
       std::vector<std::string>{"Invalid SMT response \"\""});
   }
 }
@@ -80,15 +81,17 @@ TEST_CASE("Validation of SMT error response", "[core][smt2_incremental]")
 {
   CHECK(
     *validate_smt_response(
-       *smt2irep("(error \"Test error message.\")").parsed_output)
+       *smt2irep("(error \"Test error message.\")").parsed_output, {})
        .get_if_valid() == smt_error_responset{"Test error message."});
   CHECK(
-    *validate_smt_response(*smt2irep("(error)").parsed_output).get_if_error() ==
+    *validate_smt_response(*smt2irep("(error)").parsed_output, {})
+       .get_if_error() ==
     std::vector<std::string>{"Error response is missing the error message."});
   CHECK(
     *validate_smt_response(
        *smt2irep("(error \"Test error message1.\" \"Test error message2.\")")
-          .parsed_output)
+          .parsed_output,
+       {})
        .get_if_error() ==
     std::vector<std::string>{"Error response has multiple error messages - \"\n"
                              "0: error\n"
@@ -101,14 +104,14 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
   SECTION("Boolean sorted values.")
   {
     const response_or_errort<smt_responset> true_response =
-      validate_smt_response(*smt2irep("((a true))").parsed_output);
+      validate_smt_response(*smt2irep("((a true))").parsed_output, {});
     CHECK(
       *true_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
         smt_identifier_termt{"a", smt_bool_sortt{}},
         smt_bool_literal_termt{true}}}});
     const response_or_errort<smt_responset> false_response =
-      validate_smt_response(*smt2irep("((a false))").parsed_output);
+      validate_smt_response(*smt2irep("((a false))").parsed_output, {});
     CHECK(
       *false_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -120,7 +123,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     SECTION("Hex value")
     {
       const response_or_errort<smt_responset> response_255 =
-        validate_smt_response(*smt2irep("((a #xff))").parsed_output);
+        validate_smt_response(*smt2irep("((a #xff))").parsed_output, {});
       CHECK(
         *response_255.get_if_valid() ==
         smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -130,7 +133,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     SECTION("Binary value")
     {
       const response_or_errort<smt_responset> response_42 =
-        validate_smt_response(*smt2irep("((a #b00101010))").parsed_output);
+        validate_smt_response(*smt2irep("((a #b00101010))").parsed_output, {});
       CHECK(
         *response_42.get_if_valid() ==
         smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -140,7 +143,8 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     SECTION("Descriptors which are bit vector constants")
     {
       const response_or_errort<smt_responset> response_descriptor =
-        validate_smt_response(*smt2irep("(((_ bv255 8) #x2A))").parsed_output);
+        validate_smt_response(
+          *smt2irep("(((_ bv255 8) #x2A))").parsed_output, {});
       CHECK(
         *response_descriptor.get_if_valid() ==
         smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -152,7 +156,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
         {
           const response_or_errort<smt_responset> pair_value_response =
             validate_smt_response(
-              *smt2irep("(((_ bv256 8) #xff))").parsed_output);
+              *smt2irep("(((_ bv256 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
             std::vector<std::string>{
@@ -164,7 +168,8 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
         SECTION("Value missing bv prefix.")
         {
           const response_or_errort<smt_responset> pair_value_response =
-            validate_smt_response(*smt2irep("(((_ 42 8) #xff))").parsed_output);
+            validate_smt_response(
+              *smt2irep("(((_ 42 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
             std::vector<std::string>{
@@ -177,7 +182,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
         {
           const response_or_errort<smt_responset> pair_value_response =
             validate_smt_response(
-              *smt2irep("(((_ bv2A 8) #xff))").parsed_output);
+              *smt2irep("(((_ bv2A 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
             std::vector<std::string>{
@@ -190,7 +195,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
         {
           const response_or_errort<smt_responset> pair_value_response =
             validate_smt_response(
-              *smt2irep("(((_ bv0 0) #xff))").parsed_output);
+              *smt2irep("(((_ bv0 0) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
             std::vector<std::string>{
@@ -205,7 +210,8 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
   SECTION("Multiple valuation pairs.")
   {
     const response_or_errort<smt_responset> two_pair_response =
-      validate_smt_response(*smt2irep("((a true) (b false))").parsed_output);
+      validate_smt_response(
+        *smt2irep("((a true) (b false))").parsed_output, {});
     CHECK(
       *two_pair_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -218,12 +224,13 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
   SECTION("Invalid terms.")
   {
     const response_or_errort<smt_responset> empty_value_response =
-      validate_smt_response(*smt2irep("((a ())))").parsed_output);
+      validate_smt_response(*smt2irep("((a ())))").parsed_output, {});
     CHECK(
       *empty_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\"."});
     const response_or_errort<smt_responset> pair_value_response =
-      validate_smt_response(*smt2irep("((a (#xF00D #xBAD))))").parsed_output);
+      validate_smt_response(
+        *smt2irep("((a (#xF00D #xBAD))))").parsed_output, {});
     CHECK(
       *pair_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\n"
@@ -231,7 +238,8 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
                                "1: #xBAD\"."});
     const response_or_errort<smt_responset> two_pair_value_response =
       validate_smt_response(
-        *smt2irep("((a (#xF00D #xBAD)) (b (#xDEAD #xFA11)))").parsed_output);
+        *smt2irep("((a (#xF00D #xBAD)) (b (#xDEAD #xFA11)))").parsed_output,
+        {});
     CHECK(
       *two_pair_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\n"
@@ -241,12 +249,12 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
                                "0: #xDEAD\n"
                                "1: #xFA11\"."});
     const response_or_errort<smt_responset> empty_descriptor_response =
-      validate_smt_response(*smt2irep("((() true))").parsed_output);
+      validate_smt_response(*smt2irep("((() true))").parsed_output, {});
     CHECK(
       *empty_descriptor_response.get_if_error() ==
       std::vector<std::string>{"Expected descriptor SMT term, found - \"\"."});
     const response_or_errort<smt_responset> empty_pair =
-      validate_smt_response(*smt2irep("((() ())))").parsed_output);
+      validate_smt_response(*smt2irep("((() ())))").parsed_output, {});
     CHECK(
       *empty_pair.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\"."});

From 84c8705a8431f9d03024e726e2dce465f4b3a41f Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 21 Jul 2022 14:49:05 +0100
Subject: [PATCH 02/11] Update smt_response validation to account for known
 identifiers

---
 .../smt_response_validation.cpp               | 58 ++++++-------
 .../smt_response_validation.cpp               | 81 ++++++++++++-------
 2 files changed, 74 insertions(+), 65 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
index 941b789bcf2..d842c061820 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -271,52 +271,33 @@ valid_smt_bit_vector_constant(const irept &parse_tree)
   return {};
 }
 
-static optionalt<smt_termt> valid_term(const irept &parse_tree)
+static response_or_errort<smt_termt> validate_term(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   if(const auto smt_bool = valid_smt_bool(parse_tree))
-    return {*smt_bool};
+    return response_or_errort<smt_termt>{*smt_bool};
   if(const auto bit_vector_constant = valid_smt_bit_vector_constant(parse_tree))
-    return {*bit_vector_constant};
-  return {};
-}
+    return response_or_errort<smt_termt>{*bit_vector_constant};
+  const auto find_result = identifier_table.find(parse_tree.id());
+  if(find_result != identifier_table.end())
+    return response_or_errort<smt_termt>{find_result->second};
 
-static response_or_errort<smt_termt> validate_term(const irept &parse_tree)
-{
-  if(const auto term = valid_term(parse_tree))
-    return response_or_errort<smt_termt>{*term};
   return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
                                        print_parse_tree(parse_tree) + "\"."};
 }
 
-static response_or_errort<smt_termt>
-validate_smt_descriptor(const irept &parse_tree, const smt_sortt &sort)
-{
-  if(const auto term = valid_term(parse_tree))
-    return response_or_errort<smt_termt>{*term};
-  const auto id = parse_tree.id();
-  if(!id.empty())
-    return response_or_errort<smt_termt>{smt_identifier_termt{id, sort}};
-  return response_or_errort<smt_termt>{
-    "Expected descriptor SMT term, found - \"" + print_parse_tree(parse_tree) +
-    "\"."};
-}
-
 static response_or_errort<smt_get_value_responset::valuation_pairt>
-validate_valuation_pair(const irept &pair_parse_tree)
+validate_valuation_pair(
+  const irept &pair_parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   PRECONDITION(pair_parse_tree.get_sub().size() == 2);
   const auto &descriptor = pair_parse_tree.get_sub()[0];
   const auto &value = pair_parse_tree.get_sub()[1];
-  const response_or_errort<smt_termt> value_validation = validate_term(value);
-  if(const auto value_errors = value_validation.get_if_error())
-  {
-    return response_or_errort<smt_get_value_responset::valuation_pairt>{
-      *value_errors};
-  }
-  const smt_termt value_term = *value_validation.get_if_valid();
   return validation_propagating<smt_get_value_responset::valuation_pairt>(
-    validate_smt_descriptor(descriptor, value_term.get_sort()),
-    validate_term(value));
+    validate_term(descriptor, identifier_table),
+    validate_term(value, identifier_table));
 }
 
 /// \returns: A response or error in the case where the parse tree appears to be
@@ -325,7 +306,9 @@ validate_valuation_pair(const irept &pair_parse_tree)
 ///   keyword, it will be considered that the response is intended to be a
 ///   get-value response if it is composed of a collection of one or more pairs.
 static optionalt<response_or_errort<smt_responset>>
-valid_smt_get_value_response(const irept &parse_tree)
+valid_smt_get_value_response(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   // Shape matching for does this look like a get value response?
   if(!parse_tree.id().empty())
@@ -338,7 +321,8 @@ valid_smt_get_value_response(const irept &parse_tree)
   std::vector<smt_get_value_responset::valuation_pairt> valuation_pairs;
   for(const auto &pair : parse_tree.get_sub())
   {
-    const auto pair_validation_result = validate_valuation_pair(pair);
+    const auto pair_validation_result =
+      validate_valuation_pair(pair, identifier_table);
     if(const auto error = pair_validation_result.get_if_error())
       error_messages.insert(error_messages.end(), error->begin(), error->end());
     if(const auto valid_pair = pair_validation_result.get_if_valid())
@@ -372,8 +356,12 @@ response_or_errort<smt_responset> validate_smt_response(
     return response_or_errort<smt_responset>{smt_success_responset{}};
   if(parse_tree.id() == "unsupported")
     return response_or_errort<smt_responset>{smt_unsupported_responset{}};
-  if(const auto get_value_response = valid_smt_get_value_response(parse_tree))
+  if(
+    const auto get_value_response =
+      valid_smt_get_value_response(parse_tree, identifier_table))
+  {
     return *get_value_response;
+  }
   return response_or_errort<smt_responset>{"Invalid SMT response \"" +
                                            id2string(parse_tree.id()) + "\""};
 }
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
index 6eb674f7ce1..6b7e41e4fc3 100644
--- a/unit/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -101,17 +101,32 @@ TEST_CASE("Validation of SMT error response", "[core][smt2_incremental]")
 
 TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
 {
+  const auto table_with_identifiers =
+    [](const std::vector<std::pair<std::string, smt_sortt>> &identifiers) {
+      std::unordered_map<irep_idt, smt_identifier_termt> table;
+      for(auto &identifier_pair : identifiers)
+      {
+        auto &identifier = identifier_pair.first;
+        auto &sort = identifier_pair.second;
+        table.insert({identifier, smt_identifier_termt{identifier, sort}});
+      }
+      return table;
+    };
   SECTION("Boolean sorted values.")
   {
+    const auto identifier_table =
+      table_with_identifiers({{"a", smt_bool_sortt{}}});
     const response_or_errort<smt_responset> true_response =
-      validate_smt_response(*smt2irep("((a true))").parsed_output, {});
+      validate_smt_response(
+        *smt2irep("((a true))").parsed_output, identifier_table);
     CHECK(
       *true_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
         smt_identifier_termt{"a", smt_bool_sortt{}},
         smt_bool_literal_termt{true}}}});
     const response_or_errort<smt_responset> false_response =
-      validate_smt_response(*smt2irep("((a false))").parsed_output, {});
+      validate_smt_response(
+        *smt2irep("((a false))").parsed_output, identifier_table);
     CHECK(
       *false_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -120,10 +135,13 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
   }
   SECTION("Bit vector sorted values.")
   {
+    const auto identifier_table =
+      table_with_identifiers({{"a", smt_bit_vector_sortt{8}}});
     SECTION("Hex value")
     {
       const response_or_errort<smt_responset> response_255 =
-        validate_smt_response(*smt2irep("((a #xff))").parsed_output, {});
+        validate_smt_response(
+          *smt2irep("((a #xff))").parsed_output, identifier_table);
       CHECK(
         *response_255.get_if_valid() ==
         smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -133,7 +151,8 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     SECTION("Binary value")
     {
       const response_or_errort<smt_responset> response_42 =
-        validate_smt_response(*smt2irep("((a #b00101010))").parsed_output, {});
+        validate_smt_response(
+          *smt2irep("((a #b00101010))").parsed_output, identifier_table);
       CHECK(
         *response_42.get_if_valid() ==
         smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -159,11 +178,10 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
               *smt2irep("(((_ bv256 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
-            std::vector<std::string>{
-              "Expected descriptor SMT term, found - \"\n"
-              "0: _\n"
-              "1: bv256\n"
-              "2: 8\"."});
+            std::vector<std::string>{"Unrecognised SMT term - \"\n"
+                                     "0: _\n"
+                                     "1: bv256\n"
+                                     "2: 8\"."});
         }
         SECTION("Value missing bv prefix.")
         {
@@ -172,11 +190,10 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
               *smt2irep("(((_ 42 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
-            std::vector<std::string>{
-              "Expected descriptor SMT term, found - \"\n"
-              "0: _\n"
-              "1: 42\n"
-              "2: 8\"."});
+            std::vector<std::string>{"Unrecognised SMT term - \"\n"
+                                     "0: _\n"
+                                     "1: 42\n"
+                                     "2: 8\"."});
         }
         SECTION("Hex value.")
         {
@@ -185,11 +202,10 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
               *smt2irep("(((_ bv2A 8) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
-            std::vector<std::string>{
-              "Expected descriptor SMT term, found - \"\n"
-              "0: _\n"
-              "1: bv2A\n"
-              "2: 8\"."});
+            std::vector<std::string>{"Unrecognised SMT term - \"\n"
+                                     "0: _\n"
+                                     "1: bv2A\n"
+                                     "2: 8\"."});
         }
         SECTION("Zero width.")
         {
@@ -198,20 +214,21 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
               *smt2irep("(((_ bv0 0) #xff))").parsed_output, {});
           CHECK(
             *pair_value_response.get_if_error() ==
-            std::vector<std::string>{
-              "Expected descriptor SMT term, found - \"\n"
-              "0: _\n"
-              "1: bv0\n"
-              "2: 0\"."});
+            std::vector<std::string>{"Unrecognised SMT term - \"\n"
+                                     "0: _\n"
+                                     "1: bv0\n"
+                                     "2: 0\"."});
         }
       }
     }
   }
   SECTION("Multiple valuation pairs.")
   {
+    const auto identifier_table = table_with_identifiers(
+      {{"a", smt_bool_sortt{}}, {"b", smt_bool_sortt{}}});
     const response_or_errort<smt_responset> two_pair_response =
       validate_smt_response(
-        *smt2irep("((a true) (b false))").parsed_output, {});
+        *smt2irep("((a true) (b false))").parsed_output, identifier_table);
     CHECK(
       *two_pair_response.get_if_valid() ==
       smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
@@ -223,14 +240,17 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
   }
   SECTION("Invalid terms.")
   {
+    const auto identifier_table = table_with_identifiers(
+      {{"a", smt_bit_vector_sortt{16}}, {"b", smt_bit_vector_sortt{16}}});
     const response_or_errort<smt_responset> empty_value_response =
-      validate_smt_response(*smt2irep("((a ())))").parsed_output, {});
+      validate_smt_response(
+        *smt2irep("((a ())))").parsed_output, identifier_table);
     CHECK(
       *empty_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\"."});
     const response_or_errort<smt_responset> pair_value_response =
       validate_smt_response(
-        *smt2irep("((a (#xF00D #xBAD))))").parsed_output, {});
+        *smt2irep("((a (#xF00D #xBAD))))").parsed_output, identifier_table);
     CHECK(
       *pair_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\n"
@@ -239,7 +259,7 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     const response_or_errort<smt_responset> two_pair_value_response =
       validate_smt_response(
         *smt2irep("((a (#xF00D #xBAD)) (b (#xDEAD #xFA11)))").parsed_output,
-        {});
+        identifier_table);
     CHECK(
       *two_pair_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\n"
@@ -252,11 +272,12 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
       validate_smt_response(*smt2irep("((() true))").parsed_output, {});
     CHECK(
       *empty_descriptor_response.get_if_error() ==
-      std::vector<std::string>{"Expected descriptor SMT term, found - \"\"."});
+      std::vector<std::string>{"Unrecognised SMT term - \"\"."});
     const response_or_errort<smt_responset> empty_pair =
       validate_smt_response(*smt2irep("((() ())))").parsed_output, {});
     CHECK(
       *empty_pair.get_if_error() ==
-      std::vector<std::string>{"Unrecognised SMT term - \"\"."});
+      std::vector<std::string>{
+        "Unrecognised SMT term - \"\".", "Unrecognised SMT term - \"\"."});
   }
 }

From f1eb62cf2a020914dd8968c9b772c45a3f372649 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Thu, 21 Jul 2022 17:04:38 +0100
Subject: [PATCH 03/11] Add validation of `select` to smt_response_validation

---
 .../smt_response_validation.cpp               | 37 ++++++++++++++++++-
 .../smt_response_validation.cpp               | 33 +++++++++++++++--
 2 files changed, 66 insertions(+), 4 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
index d842c061820..714f3f841fd 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -21,8 +21,14 @@
 #include <util/mp_arith.h>
 #include <util/range.h>
 
+#include "smt_array_theory.h"
+
 #include <regex>
 
+static response_or_errort<smt_termt> validate_term(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
+
 template <class smtt>
 response_or_errort<smtt>::response_or_errort(smtt smt) : smt{std::move(smt)}
 {
@@ -271,6 +277,30 @@ valid_smt_bit_vector_constant(const irept &parse_tree)
   return {};
 }
 
+static optionalt<response_or_errort<smt_termt>> try_select_validation(
+  const irept &parse_tree,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+{
+  if(parse_tree.get_sub().empty())
+    return {};
+  if(parse_tree.get_sub()[0].id() != "select")
+    return {};
+  if(parse_tree.get_sub().size() != 3)
+  {
+    return response_or_errort<smt_termt>{
+      "\"select\" is expected to have 2 arguments, but " +
+      std::to_string(parse_tree.get_sub().size()) +
+      " arguments were found - \"" + print_parse_tree(parse_tree) + "\"."};
+  }
+  const auto array = validate_term(parse_tree.get_sub()[1], identifier_table);
+  const auto index = validate_term(parse_tree.get_sub()[2], identifier_table);
+  const auto messages = collect_messages(array, index);
+  if(!messages.empty())
+    return response_or_errort<smt_termt>{messages};
+  return response_or_errort<smt_termt>{
+    smt_array_theoryt::select(*array.get_if_valid(), *index.get_if_valid())};
+}
+
 static response_or_errort<smt_termt> validate_term(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
@@ -282,7 +312,12 @@ static response_or_errort<smt_termt> validate_term(
   const auto find_result = identifier_table.find(parse_tree.id());
   if(find_result != identifier_table.end())
     return response_or_errort<smt_termt>{find_result->second};
-
+  if(
+    const auto select_validation =
+      try_select_validation(parse_tree, identifier_table))
+  {
+    return *select_validation;
+  }
   return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
                                        print_parse_tree(parse_tree) + "\"."};
 }
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
index 6b7e41e4fc3..f0dd6e12971 100644
--- a/unit/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -1,10 +1,11 @@
 // Author: Diffblue Ltd.
 
-#include <testing-utils/smt2irep.h>
-#include <testing-utils/use_catch.h>
+#include <util/mp_arith.h>
 
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_response_validation.h>
-#include <util/mp_arith.h>
+#include <testing-utils/smt2irep.h>
+#include <testing-utils/use_catch.h>
 
 // Debug printer for `smt_responset`. This will be used by the catch framework
 // for printing in the case of failed checks / requirements.
@@ -159,6 +160,32 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
           smt_identifier_termt{"a", smt_bit_vector_sortt{8}},
           smt_bit_vector_constant_termt{42, 8}}}});
     }
+    SECTION("Array values")
+    {
+      // Construction of select part of response
+      const smt_bit_vector_constant_termt index_term(
+        0xA, smt_bit_vector_sortt(32));
+      const smt_sortt value_sort(smt_bit_vector_sortt(32));
+      const smt_identifier_termt array_term(
+        "b", smt_array_sortt(index_term.get_sort(), value_sort));
+      const smt_function_application_termt select =
+        smt_array_theoryt::select(array_term, index_term);
+      // Identifier table needs to contain identifier of array
+      const auto identifier_table = table_with_identifiers(
+        {{"b",
+          smt_array_sortt{
+            smt_bit_vector_sortt{32}, smt_bit_vector_sortt{32}}}});
+
+      const response_or_errort<smt_responset> response_get_select =
+        validate_smt_response(
+          *smt2irep("(((select |b| (_ bv10 32)) #x0000002a))").parsed_output,
+          identifier_table);
+
+      CHECK(
+        *response_get_select.get_if_valid() ==
+        smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
+          select, smt_bit_vector_constant_termt{0x2A, 32}}}});
+    }
     SECTION("Descriptors which are bit vector constants")
     {
       const response_or_errort<smt_responset> response_descriptor =

From 4fe1831a5d430de289a2bb8d3d51556e7519ec49 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Mon, 15 Aug 2022 17:00:46 +0100
Subject: [PATCH 04/11] Build identifier_table in SMT incremental decision
 procedure

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
---
 .../smt2_incremental_decision_procedure.cpp        | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index c8ce014e30a..db47865f3ac 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -85,6 +85,7 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
   const array_exprt &array,
   const smt_identifier_termt &array_identifier)
 {
+  identifier_table.emplace(array_identifier.identifier(), array_identifier);
   const std::vector<exprt> &elements = array.operands();
   const typet &index_type = array.type().index_type();
   for(std::size_t i = 0; i < elements.size(); ++i)
@@ -136,13 +137,15 @@ void send_function_definition(
   const irep_idt &symbol_identifier,
   const std::unique_ptr<smt_base_solver_processt> &solver_process,
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
-    &expression_identifiers)
+    &expression_identifiers,
+  std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   const smt_declare_function_commandt function{
     smt_identifier_termt(
       symbol_identifier, convert_type_to_smt_sort(expr.type())),
     {}};
   expression_identifiers.emplace(expr, function.identifier());
+  identifier_table.emplace(symbol_identifier, function.identifier());
   solver_process->send(function);
 }
 
@@ -184,7 +187,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
           *symbol_expr,
           symbol_expr->get_identifier(),
           solver_process,
-          expression_identifiers);
+          expression_identifiers,
+          identifier_table);
       }
       else
       {
@@ -193,6 +197,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         const smt_define_function_commandt function{
           symbol->name, {}, convert_expr_to_smt(symbol->value)};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
+        identifier_table.emplace(identifier, function.identifier());
         solver_process->send(function);
       }
     }
@@ -211,7 +216,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         *nondet_symbol,
         nondet_symbol->get_identifier(),
         solver_process,
-        expression_identifiers);
+        expression_identifiers,
+        identifier_table);
     }
     to_be_defined.pop();
   }
@@ -264,6 +270,8 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   smt_define_function_commandt function{
     "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
   expression_handle_identifiers.emplace(expr, function.identifier());
+  identifier_table.emplace(
+    function.identifier().identifier(), function.identifier());
   solver_process->send(function);
 }
 

From b257100d3011998035173b76f6fdcccd609cc34b Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 15 Jul 2022 17:44:32 +0100
Subject: [PATCH 05/11] Fetch value of array elements individually from solver

---
 .../smt2_incremental_decision_procedure.cpp   | 75 ++++++++++++++-----
 .../smt2_incremental_decision_procedure.h     |  6 ++
 .../smt2_incremental_decision_procedure.cpp   | 21 ++++++
 3 files changed, 85 insertions(+), 17 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index db47865f3ac..79fbe6f9534 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -319,6 +319,59 @@ static optionalt<smt_termt> get_identifier(
   return {};
 }
 
+array_exprt smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &array,
+  const array_typet &type) const
+{
+  INVARIANT(
+    type.is_complete(), "Array size is required for getting array values.");
+  const auto size = numeric_cast<std::size_t>(get(type.size()));
+  INVARIANT(
+    size,
+    "Size of array must be convertible to std::size_t for getting array value");
+  std::vector<exprt> elements;
+  const auto index_type = type.index_type();
+  elements.reserve(*size);
+  for(std::size_t index = 0; index < size; ++index)
+  {
+    elements.push_back(get_expr(
+      smt_array_theoryt::select(
+        array,
+        ::convert_expr_to_smt(
+          from_integer(index, index_type),
+          object_map,
+          pointer_sizes_map,
+          object_size_function.make_application)),
+      type.element_type()));
+  }
+  return array_exprt{elements, type};
+}
+
+exprt smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &descriptor,
+  const typet &type) const
+{
+  const smt_get_value_commandt get_value_command{descriptor};
+  const smt_responset response = get_response_to_command(
+    *solver_process, get_value_command, identifier_table);
+  const auto get_value_response = response.cast<smt_get_value_responset>();
+  if(!get_value_response)
+  {
+    throw analysis_exceptiont{
+      "Expected get-value response from solver, but received - " +
+      response.pretty()};
+  }
+  if(get_value_response->pairs().size() > 1)
+  {
+    throw analysis_exceptiont{
+      "Expected single valuation pair in get-value response from solver, but "
+      "received multiple pairs - " +
+      response.pretty()};
+  }
+  return construct_value_expr_from_smt(
+    get_value_response->pairs()[0].get().value(), type);
+}
+
 exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
 {
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
@@ -359,25 +412,13 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
       return expr;
     }
   }
-  const smt_get_value_commandt get_value_command{*descriptor};
-  const smt_responset response = get_response_to_command(
-    *solver_process, get_value_command, identifier_table);
-  const auto get_value_response = response.cast<smt_get_value_responset>();
-  if(!get_value_response)
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
   {
-    throw analysis_exceptiont{
-      "Expected get-value response from solver, but received - " +
-      response.pretty()};
-  }
-  if(get_value_response->pairs().size() > 1)
-  {
-    throw analysis_exceptiont{
-      "Expected single valuation pair in get-value response from solver, but "
-      "received multiple pairs - " +
-      response.pretty()};
+    if(array_type->is_incomplete())
+      return expr;
+    return get_expr(*descriptor, *array_type);
   }
-  return construct_value_expr_from_smt(
-    get_value_response->pairs()[0].get().value(), expr.type());
+  return get_expr(*descriptor, expr.type());
 }
 
 void smt2_incremental_decision_proceduret::print_assignment(
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index e951196fc30..24decfa60e7 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -52,6 +52,12 @@ class smt2_incremental_decision_proceduret final
   void push() override;
   void pop() override;
 
+  /// Gets the value of \p descriptor from the solver and returns the solver
+  /// response expressed as an exprt of type \p type. This is an implementation
+  /// detail of the `get(exprt)` member function.
+  exprt get_expr(const smt_termt &descriptor, const typet &type) const;
+  array_exprt get_expr(const smt_termt &array, const array_typet &type) const;
+
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 95d4b598f67..e6f5a1ba1b8 100644
--- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -616,6 +616,27 @@ TEST_CASE(
       smt_assert_commandt{smt_core_theoryt::equal(
         foo_term, smt_array_theoryt::select(array_term, index_term))}};
     REQUIRE(test.sent_commands == expected_commands);
+
+    SECTION("Get values of array literal")
+    {
+      test.sent_commands.clear();
+      test.mock_responses = {
+        // get-value response for array_size
+        smt_get_value_responset{
+          {{{smt_bit_vector_constant_termt{2, 32}},
+            smt_bit_vector_constant_termt{2, 32}}}},
+        // get-value response for first element
+        smt_get_value_responset{
+          {{{smt_array_theoryt::select(
+              array_term, smt_bit_vector_constant_termt{0, 32})},
+            smt_bit_vector_constant_termt{9, 8}}}},
+        // get-value response for second element
+        smt_get_value_responset{
+          {{{smt_array_theoryt::select(
+              array_term, smt_bit_vector_constant_termt{1, 32})},
+            smt_bit_vector_constant_termt{12, 8}}}}};
+      REQUIRE(test.procedure.get(array_literal) == array_literal);
+    }
   }
   SECTION("array_of_exprt - all elements set to a given value")
   {

From dea65004a64a5f00710e847c891fe9f63127076e Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 11 Aug 2022 10:01:17 +0100
Subject: [PATCH 06/11] Add regression tests for array read traces

---
 .../cbmc-incr-smt2/arrays_traces/array_read.c     |  7 +++++++
 .../cbmc-incr-smt2/arrays_traces/array_read.desc  | 15 +++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/arrays_traces/array_read.c
 create mode 100644 regression/cbmc-incr-smt2/arrays_traces/array_read.desc

diff --git a/regression/cbmc-incr-smt2/arrays_traces/array_read.c b/regression/cbmc-incr-smt2/arrays_traces/array_read.c
new file mode 100644
index 00000000000..0509fd03d23
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays_traces/array_read.c
@@ -0,0 +1,7 @@
+int main()
+{
+  int example_array[1025];
+  unsigned int index;
+  __CPROVER_assume(index < 1025);
+  __CPROVER_assert(example_array[index] != 42, "Array condition");
+}
diff --git a/regression/cbmc-incr-smt2/arrays_traces/array_read.desc b/regression/cbmc-incr-smt2/arrays_traces/array_read.desc
new file mode 100644
index 00000000000..f9d3522ec42
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays_traces/array_read.desc
@@ -0,0 +1,15 @@
+CORE
+array_read.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: FAILURE
+^Trace for main\.assertion\.1
+example_array=\{ (\d+, )*42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading a value at a non-deterministic index of an array.
+Similar to the test in ../arrays/array_read.c, but we want to assert
+the value of the array that comes back in the trace to make sure we're
+observing the correct values.

From bbf7a82e330e7dac5fbe8525b91a84ba51bddf62 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 12 Aug 2022 13:02:44 +0100
Subject: [PATCH 07/11] Define smt functions for index expressions

So that the value of the index can be fetched when building traces based
on requesting the index identifier.
---
 .../smt2_incremental_decision_procedure.cpp   | 22 +++++++++++++++++++
 .../smt2_incremental_decision_procedure.h     |  3 ++-
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 79fbe6f9534..c8f5c595d7d 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -275,9 +275,31 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   solver_process->send(function);
 }
 
+void smt2_incremental_decision_proceduret::define_index_identifiers(
+  const exprt &expr)
+{
+  expr.visit_pre([&](const exprt &expr_node) {
+    if(!can_cast_type<array_typet>(expr_node.type()))
+      return;
+    if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
+    {
+      const auto index_expr = with_expr->where();
+      const auto index_term = convert_expr_to_smt(index_expr);
+      const auto index_identifier = "index_" + std::to_string(index_sequence());
+      const auto index_definition =
+        smt_define_function_commandt{index_identifier, {}, index_term};
+      expression_identifiers.emplace(index_expr, index_definition.identifier());
+      identifier_table.emplace(index_identifier, index_definition.identifier());
+      solver_process->send(
+        smt_define_function_commandt{index_identifier, {}, index_term});
+    }
+  });
+}
+
 smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
+  define_index_identifiers(expr);
   const exprt substituted =
     substitute_identifiers(expr, expression_identifiers);
   track_expression_objects(substituted, ns, object_map);
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
index 24decfa60e7..67fcbbbd919 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -91,6 +91,7 @@ class smt2_incremental_decision_proceduret final
   /// \brief Add objects in \p expr to object_map if needed and convert to smt.
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
+  void define_index_identifiers(const exprt &expr);
   /// Sends the solver the definitions of the object sizes.
   void define_object_sizes();
 
@@ -118,7 +119,7 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence, array_sequence;
+  } handle_sequence, array_sequence, index_sequence;
   /// When the `handle(exprt)` member function is called, the decision procedure
   /// commands the SMT solver to define a new function corresponding to the
   /// given expression. The mapping of the expressions to the function

From 780d6cc17d5381c436f1c29f784b90a3dd3c3160 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Fri, 12 Aug 2022 18:30:47 +0100
Subject: [PATCH 08/11] Implement get of array index values in smt decision
 procedure

So that writes to arrays can be shown in traces.
---
 .../smt2_incremental_decision_procedure.cpp   | 21 ++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index c8f5c595d7d..9e62784a405 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -399,9 +399,24 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`get` - \n  " + expr.pretty(2, 0) << messaget::eom;
   });
-  optionalt<smt_termt> descriptor =
-    get_identifier(expr, expression_handle_identifiers, expression_identifiers);
-
+  auto descriptor = [&]() -> optionalt<smt_termt> {
+    if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
+    {
+      const auto array = get_identifier(
+        index_expr->array(),
+        expression_handle_identifiers,
+        expression_identifiers);
+      const auto index = get_identifier(
+        index_expr->index(),
+        expression_handle_identifiers,
+        expression_identifiers);
+      if(!array || !index)
+        return {};
+      return smt_array_theoryt::select(*array, *index);
+    }
+    return get_identifier(
+      expr, expression_handle_identifiers, expression_identifiers);
+  }();
   if(!descriptor)
   {
     if(gather_dependent_expressions(expr).empty())

From d60f030f576f56d3ffab7477fdaf65693f7842d3 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 17 Aug 2022 20:04:20 +0100
Subject: [PATCH 09/11] Add regression tests for array write traces

---
 .../cbmc-incr-smt2/arrays_traces/array_write.c       |  9 +++++++++
 .../cbmc-incr-smt2/arrays_traces/array_write.desc    | 12 ++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/arrays_traces/array_write.c
 create mode 100644 regression/cbmc-incr-smt2/arrays_traces/array_write.desc

diff --git a/regression/cbmc-incr-smt2/arrays_traces/array_write.c b/regression/cbmc-incr-smt2/arrays_traces/array_write.c
new file mode 100644
index 00000000000..2796e847b7a
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays_traces/array_write.c
@@ -0,0 +1,9 @@
+int main()
+{
+  int example_array[1025];
+  unsigned int index;
+  __CPROVER_assume(index < 1025);
+  example_array[index] = 42;
+  __CPROVER_assert(example_array[index] == 42, "Array condition");
+  __CPROVER_assert(example_array[index] != 42, "Array condition");
+}
diff --git a/regression/cbmc-incr-smt2/arrays_traces/array_write.desc b/regression/cbmc-incr-smt2/arrays_traces/array_write.desc
new file mode 100644
index 00000000000..19828b6cb11
--- /dev/null
+++ b/regression/cbmc-incr-smt2/arrays_traces/array_write.desc
@@ -0,0 +1,12 @@
+CORE
+array_write.c
+--trace
+Passing problem to incremental SMT2 solving
+^Trace for main\.assertion\.2
+example_array\[\d{1,4}ll?\]=42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of writing a value at a non-deterministic index of an array, then asserting
+the value we expect.

From 787b3c10d3e03e1792367218742fe2482efb4b54 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 24 Aug 2022 18:09:30 +0100
Subject: [PATCH 10/11] Add unit test for validation of unknown identifiers

---
 unit/solvers/smt2_incremental/smt_response_validation.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
index f0dd6e12971..a6bfd9edb55 100644
--- a/unit/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -275,6 +275,14 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
     CHECK(
       *empty_value_response.get_if_error() ==
       std::vector<std::string>{"Unrecognised SMT term - \"\"."});
+    const response_or_errort<smt_responset> unknown_identifier_response =
+      validate_smt_response(
+        *smt2irep("((foo bar)))").parsed_output, identifier_table);
+    CHECK(
+      *unknown_identifier_response.get_if_error() ==
+      std::vector<std::string>{
+        "Unrecognised SMT term - \"foo\".",
+        "Unrecognised SMT term - \"bar\"."});
     const response_or_errort<smt_responset> pair_value_response =
       validate_smt_response(
         *smt2irep("((a (#xF00D #xBAD))))").parsed_output, identifier_table);

From 0f7b21c879324f92077804cc5ba42da7f0a7e3ed Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Wed, 31 Aug 2022 21:08:24 +0100
Subject: [PATCH 11/11] Add validation for array select argument sorts

---
 .../smt2_incremental/response_or_error.h      | 64 +++++++++++++++++++
 .../smt2_incremental/smt_array_theory.cpp     | 19 ++++--
 .../smt2_incremental/smt_array_theory.h       |  2 +
 .../smt_response_validation.cpp               | 43 +------------
 .../smt_response_validation.h                 | 34 +---------
 src/solvers/smt2_incremental/smt_terms.h      | 15 +++++
 .../smt_response_validation.cpp               | 43 ++++++++++---
 7 files changed, 133 insertions(+), 87 deletions(-)
 create mode 100644 src/solvers/smt2_incremental/response_or_error.h

diff --git a/src/solvers/smt2_incremental/response_or_error.h b/src/solvers/smt2_incremental/response_or_error.h
new file mode 100644
index 00000000000..48d8eab5b66
--- /dev/null
+++ b/src/solvers/smt2_incremental/response_or_error.h
@@ -0,0 +1,64 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+
+#include <util/invariant.h>
+#include <util/optional.h>
+
+#include <string>
+#include <vector>
+
+/// Holds either a valid parsed response or response sub-tree of type \tparam
+/// smtt or a collection of message strings explaining why the given input was
+/// not valid.
+template <class smtt>
+class response_or_errort final
+{
+public:
+  explicit response_or_errort(smtt smt) : smt{std::move(smt)}
+  {
+  }
+
+  explicit response_or_errort(std::string message)
+    : messages{std::move(message)}
+  {
+  }
+
+  explicit response_or_errort(std::vector<std::string> messages)
+    : messages{std::move(messages)}
+  {
+  }
+
+  /// \brief Gets the smt response if the response is valid, or returns nullptr
+  ///   otherwise.
+  const smtt *get_if_valid() const
+  {
+    INVARIANT(
+      smt.has_value() == messages.empty(),
+      "The response_or_errort class must be in the valid state or error state, "
+      "exclusively.");
+    return smt.has_value() ? &smt.value() : nullptr;
+  }
+
+  /// \brief Gets the error messages if the response is invalid, or returns
+  ///   nullptr otherwise.
+  const std::vector<std::string> *get_if_error() const
+  {
+    INVARIANT(
+      smt.has_value() == messages.empty(),
+      "The response_or_errort class must be in the valid state or error state, "
+      "exclusively.");
+    return smt.has_value() ? nullptr : &messages;
+  }
+
+private:
+  // The below two fields could be a single `std::variant` field, if there was
+  // an implementation of it available in the cbmc repository. However at the
+  // time of writing we are targeting C++11, `std::variant` was introduced in
+  // C++17 and we have no backported version.
+  optionalt<smtt> smt;
+  std::vector<std::string> messages;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
diff --git a/src/solvers/smt2_incremental/smt_array_theory.cpp b/src/solvers/smt2_incremental/smt_array_theory.cpp
index 94cb6befb3c..bf9c8349e3b 100644
--- a/src/solvers/smt2_incremental/smt_array_theory.cpp
+++ b/src/solvers/smt2_incremental/smt_array_theory.cpp
@@ -14,15 +14,24 @@ smt_sortt smt_array_theoryt::selectt::return_sort(
   return array.get_sort().cast<smt_array_sortt>()->element_sort();
 }
 
-void smt_array_theoryt::selectt::validate(
+std::vector<std::string> smt_array_theoryt::selectt::validation_errors(
   const smt_termt &array,
   const smt_termt &index)
 {
   const auto array_sort = array.get_sort().cast<smt_array_sortt>();
-  INVARIANT(array_sort, "\"select\" may only select from an array.");
-  INVARIANT(
-    array_sort->index_sort() == index.get_sort(),
-    "Sort of arrays index must match the sort of the index supplied.");
+  if(!array_sort)
+    return {"\"select\" may only select from an array."};
+  if(array_sort->index_sort() != index.get_sort())
+    return {"Sort of arrays index must match the sort of the index supplied."};
+  return {};
+}
+
+void smt_array_theoryt::selectt::validate(
+  const smt_termt &array,
+  const smt_termt &index)
+{
+  const auto validation_errors = selectt::validation_errors(array, index);
+  INVARIANT(validation_errors.empty(), validation_errors[0]);
 }
 
 const smt_function_application_termt::factoryt<smt_array_theoryt::selectt>
diff --git a/src/solvers/smt2_incremental/smt_array_theory.h b/src/solvers/smt2_incremental/smt_array_theory.h
index d56f049d745..ed48c09df3d 100644
--- a/src/solvers/smt2_incremental/smt_array_theory.h
+++ b/src/solvers/smt2_incremental/smt_array_theory.h
@@ -13,6 +13,8 @@ class smt_array_theoryt
     static const char *identifier();
     static smt_sortt
     return_sort(const smt_termt &array, const smt_termt &index);
+    static std::vector<std::string>
+    validation_errors(const smt_termt &array, const smt_termt &index);
     static void validate(const smt_termt &array, const smt_termt &index);
   };
   static const smt_function_application_termt::factoryt<selectt> select;
diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
index 714f3f841fd..c81026ede29 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -29,45 +29,6 @@ static response_or_errort<smt_termt> validate_term(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(smtt smt) : smt{std::move(smt)}
-{
-}
-
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(std::string message)
-  : messages{std::move(message)}
-{
-}
-
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(std::vector<std::string> messages)
-  : messages{std::move(messages)}
-{
-}
-
-template <class smtt>
-const smtt *response_or_errort<smtt>::get_if_valid() const
-{
-  INVARIANT(
-    smt.has_value() == messages.empty(),
-    "The response_or_errort class must be in the valid state or error state, "
-    "exclusively.");
-  return smt.has_value() ? &smt.value() : nullptr;
-}
-
-template <class smtt>
-const std::vector<std::string> *response_or_errort<smtt>::get_if_error() const
-{
-  INVARIANT(
-    smt.has_value() == messages.empty(),
-    "The response_or_errort class must be in the valid state or error state, "
-    "exclusively.");
-  return smt.has_value() ? nullptr : &messages;
-}
-
-template class response_or_errort<smt_responset>;
-
 // Implementation detail of `collect_messages` below.
 template <typename argumentt, typename... argumentst>
 void collect_messages_impl(
@@ -297,8 +258,8 @@ static optionalt<response_or_errort<smt_termt>> try_select_validation(
   const auto messages = collect_messages(array, index);
   if(!messages.empty())
     return response_or_errort<smt_termt>{messages};
-  return response_or_errort<smt_termt>{
-    smt_array_theoryt::select(*array.get_if_valid(), *index.get_if_valid())};
+  return {smt_array_theoryt::select.validation(
+    *array.get_if_valid(), *index.get_if_valid())};
 }
 
 static response_or_errort<smt_termt> validate_term(
diff --git a/src/solvers/smt2_incremental/smt_response_validation.h b/src/solvers/smt2_incremental/smt_response_validation.h
index c98b0f2cd72..306e0bdaa5c 100644
--- a/src/solvers/smt2_incremental/smt_response_validation.h
+++ b/src/solvers/smt2_incremental/smt_response_validation.h
@@ -3,40 +3,10 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 
-#include <solvers/smt2_incremental/smt_responses.h>
-#include <util/invariant.h>
 #include <util/nodiscard.h>
-#include <util/optional.h>
-
-#include <string>
-#include <vector>
-
-/// Holds either a valid parsed response or response sub-tree of type \tparam
-/// smtt or a collection of message strings explaining why the given input was
-/// not valid.
-template <class smtt>
-class response_or_errort final
-{
-public:
-  explicit response_or_errort(smtt smt);
-  explicit response_or_errort(std::string message);
-  explicit response_or_errort(std::vector<std::string> messages);
 
-  /// \brief Gets the smt response if the response is valid, or returns nullptr
-  ///   otherwise.
-  const smtt *get_if_valid() const;
-  /// \brief Gets the error messages if the response is invalid, or returns
-  ///   nullptr otherwise.
-  const std::vector<std::string> *get_if_error() const;
-
-private:
-  // The below two fields could be a single `std::variant` field, if there was
-  // an implementation of it available in the cbmc repository. However at the
-  // time of writing we are targeting C++11, `std::variant` was introduced in
-  // C++17 and we have no backported version.
-  optionalt<smtt> smt;
-  std::vector<std::string> messages;
-};
+#include <solvers/smt2_incremental/response_or_error.h>
+#include <solvers/smt2_incremental/smt_responses.h>
 
 NODISCARD response_or_errort<smt_responset> validate_smt_response(
   const irept &parse_tree,
diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h
index 53faa567c5d..fe7e51f5f94 100644
--- a/src/solvers/smt2_incremental/smt_terms.h
+++ b/src/solvers/smt2_incremental/smt_terms.h
@@ -5,6 +5,7 @@
 
 #include <util/irep.h>
 
+#include <solvers/smt2_incremental/response_or_error.h>
 #include <solvers/smt2_incremental/smt_index.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/type_traits.h>
@@ -204,6 +205,20 @@ class smt_function_application_termt : public smt_termt
           function.identifier(), std::move(return_sort), indices(function)},
         {std::forward<argument_typest>(arguments)...}};
     }
+
+    template <typename... argument_typest>
+    response_or_errort<smt_termt>
+    validation(argument_typest &&... arguments) const
+    {
+      const auto validation_errors = function.validation_errors(arguments...);
+      if(!validation_errors.empty())
+        return response_or_errort<smt_termt>{validation_errors};
+      auto return_sort = function.return_sort(arguments...);
+      return response_or_errort<smt_termt>{smt_function_application_termt{
+        smt_identifier_termt{
+          function.identifier(), std::move(return_sort), indices(function)},
+        {std::forward<argument_typest>(arguments)...}}};
+    }
   };
 };
 
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
index a6bfd9edb55..5fe8344f6bb 100644
--- a/unit/solvers/smt2_incremental/smt_response_validation.cpp
+++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp
@@ -176,15 +176,40 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
           smt_array_sortt{
             smt_bit_vector_sortt{32}, smt_bit_vector_sortt{32}}}});
 
-      const response_or_errort<smt_responset> response_get_select =
-        validate_smt_response(
-          *smt2irep("(((select |b| (_ bv10 32)) #x0000002a))").parsed_output,
-          identifier_table);
-
-      CHECK(
-        *response_get_select.get_if_valid() ==
-        smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
-          select, smt_bit_vector_constant_termt{0x2A, 32}}}});
+      SECTION("Valid application of smt_array_theoryt::select")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select |b| (_ bv10 32)) #x0000002a))").parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_valid() ==
+          smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
+            select, smt_bit_vector_constant_termt{0x2A, 32}}}});
+      }
+      SECTION("Invalid due to selecting from non-array")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select (_ bv10 32) (_ bv10 32)) #x0000002a))")
+               .parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_error() ==
+          std::vector<std::string>{
+            "\"select\" may only select from an array."});
+      }
+      SECTION("Invalid due to selecting invalid index sort")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select |b| (_ bv10 16)) #x0000002a))").parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_error() ==
+          std::vector<std::string>{
+            "Sort of arrays index must match the sort of the index supplied."});
+      }
     }
     SECTION("Descriptors which are bit vector constants")
     {