Skip to content

Commit 6c3d1da

Browse files
committed
Include original error for invalid error error message
So that it is still possible to see the error message which was being reported.
1 parent 1b426bd commit 6c3d1da

File tree

2 files changed

+6
-2
lines changed

2 files changed

+6
-2
lines changed

src/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,8 @@ valid_smt_error_response(const irept &parse_tree)
175175
if(parse_tree.get_sub().size() > 2)
176176
{
177177
return {response_or_errort<smt_responset>{
178-
"Error response has multiple error messages."}};
178+
"Error response has multiple error messages - \"" +
179+
print_parse_tree(parse_tree) + "\"."}};
179180
}
180181
return validation_propagating<smt_error_responset, smt_responset>(
181182
validate_string_literal(parse_tree.get_sub()[1]));

unit/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,10 @@ TEST_CASE("Validation of SMT error response", "[core][smt2_incremental]")
9090
*smt2irep("(error \"Test error message1.\" \"Test error message2.\")")
9191
.parsed_output)
9292
.get_if_error() ==
93-
std::vector<std::string>{"Error response has multiple error messages."});
93+
std::vector<std::string>{"Error response has multiple error messages - \"\n"
94+
"0: error\n"
95+
"1: Test error message1.\n"
96+
"2: Test error message2.\"."});
9497
}
9598

9699
TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")

0 commit comments

Comments
 (0)