@@ -139,14 +139,14 @@ valid_smt_error_response(const irept &parse_tree)
139139 // unexpected in the parse tree is now considered to be an invalid response.
140140 if (parse_tree.get_sub ().size () == 1 )
141141 {
142- return {response_or_errort<smt_responset>{
143- " Error response is missing the error message." }};
142+ return {response_or_errort<smt_responset>{std::vector<std::string>{
143+ { " Error response is missing the error message." }} }};
144144 }
145145 if (parse_tree.get_sub ().size () > 2 )
146146 {
147- return {response_or_errort<smt_responset>{
148- " Error response has multiple error messages - \" " +
149- print_parse_tree (parse_tree) + " \" ." }};
147+ return {response_or_errort<smt_responset>{std::vector<std::string>{
148+ { " Error response has multiple error messages - \" " +
149+ print_parse_tree (parse_tree) + " \" ." }} }};
150150 }
151151 return validation_propagating<smt_error_responset, smt_responset>(
152152 validate_string_literal (parse_tree.get_sub ()[1 ]));
@@ -250,10 +250,10 @@ static std::optional<response_or_errort<smt_termt>> try_select_validation(
250250 return {};
251251 if (parse_tree.get_sub ().size () != 3 )
252252 {
253- return response_or_errort<smt_termt>{
254- " \" select\" is expected to have 2 arguments, but " +
255- std::to_string (parse_tree.get_sub ().size ()) +
256- " arguments were found - \" " + print_parse_tree (parse_tree) + " \" ." };
253+ return response_or_errort<smt_termt>{std::vector<std::string>{
254+ { " \" select\" is expected to have 2 arguments, but " +
255+ std::to_string (parse_tree.get_sub ().size ()) +
256+ " arguments were found - \" " + print_parse_tree (parse_tree) + " \" ." }} };
257257 }
258258 const auto array = validate_term (parse_tree.get_sub ()[1 ], identifier_table);
259259 const auto index = validate_term (parse_tree.get_sub ()[2 ], identifier_table);
@@ -281,8 +281,8 @@ static response_or_errort<smt_termt> validate_term(
281281 {
282282 return *select_validation;
283283 }
284- return response_or_errort<smt_termt>{" Unrecognised SMT term - \" " +
285- print_parse_tree (parse_tree) + " \" ." };
284+ return response_or_errort<smt_termt>{std::vector<std::string>{
285+ { " Unrecognised SMT term - \" " + print_parse_tree (parse_tree) + " \" ." }} };
286286}
287287
288288static response_or_errort<smt_get_value_responset::valuation_pairt>
@@ -305,10 +305,10 @@ validate_valuation_pair(
305305 if (valid_descriptor.get_sort () != valid_value.get_sort ())
306306 {
307307 return resultt{
308- " Mismatched descriptor and value sorts in - " +
309- print_parse_tree (pair_parse_tree) + " \n Descriptor has sort " +
310- smt_to_smt2_string (valid_descriptor.get_sort ()) + " \n Value has sort " +
311- smt_to_smt2_string (valid_value.get_sort ())};
308+ { " Mismatched descriptor and value sorts in - " +
309+ print_parse_tree (pair_parse_tree) + " \n Descriptor has sort " +
310+ smt_to_smt2_string (valid_descriptor.get_sort ()) + " \n Value has sort " +
311+ smt_to_smt2_string (valid_value.get_sort ())} };
312312 }
313313 // see https://github.com/diffblue/cbmc/issues/7464 for why we explicitly name
314314 // the valuation_pairt type here:
@@ -378,6 +378,6 @@ response_or_errort<smt_responset> validate_smt_response(
378378 {
379379 return *get_value_response;
380380 }
381- return response_or_errort<smt_responset>{" Invalid SMT response \" " +
382- id2string (parse_tree.id ()) + " \" " };
381+ return response_or_errort<smt_responset>{std::vector<std::string>{
382+ { " Invalid SMT response \" " + id2string (parse_tree.id ()) + " \" " }} };
383383}
0 commit comments