Skip to content

Commit 01e0f08

Browse files
committed
Implement validation of unsupported smt2 response
1 parent 838df42 commit 01e0f08

File tree

2 files changed

+9
-0
lines changed

2 files changed

+9
-0
lines changed

src/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,8 @@ response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
4848
smt_check_sat_responset{smt_unknown_responset{}}};
4949
if(parse_tree.id() == "success")
5050
return response_or_errort<smt_responset>{smt_success_responset{}};
51+
if(parse_tree.id() == "unsupported")
52+
return response_or_errort<smt_responset>{smt_unsupported_responset{}};
5153
return response_or_errort<smt_responset>{"Invalid SMT response \"" +
5254
id2string(parse_tree.id()) + "\""};
5355
}

unit/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,13 @@ TEST_CASE("Validation of SMT success response", "[core][smt2_incremental]")
5151
smt_success_responset{});
5252
}
5353

54+
TEST_CASE("Validation of SMT unsupported response", "[core][smt2_incremental]")
55+
{
56+
CHECK(
57+
*validate_smt_response(*smt2irep("unsupported").parsed_output)
58+
.get_if_valid() == smt_unsupported_responset{});
59+
}
60+
5461
TEST_CASE(
5562
"Error handling of SMT response validation",
5663
"[core][smt2_incremental]")

0 commit comments

Comments
 (0)