Skip to content

Commit f01d0ec

Browse files
committed
Add sections to existing bit vector validation unit test
To separate checks and document the feature being tested.
1 parent f59f257 commit f01d0ec

File tree

1 file changed

+20
-14
lines changed

1 file changed

+20
-14
lines changed

unit/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -117,20 +117,26 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
117117
}
118118
SECTION("Bit vector sorted values.")
119119
{
120-
const response_or_errort<smt_responset> response_255 =
121-
validate_smt_response(*smt2irep("((a #xff))").parsed_output);
122-
CHECK(
123-
*response_255.get_if_valid() ==
124-
smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
125-
smt_identifier_termt{"a", smt_bit_vector_sortt{8}},
126-
smt_bit_vector_constant_termt{255, 8}}}});
127-
const response_or_errort<smt_responset> response_42 =
128-
validate_smt_response(*smt2irep("((a #b00101010))").parsed_output);
129-
CHECK(
130-
*response_42.get_if_valid() ==
131-
smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
132-
smt_identifier_termt{"a", smt_bit_vector_sortt{8}},
133-
smt_bit_vector_constant_termt{42, 8}}}});
120+
SECTION("Hex value")
121+
{
122+
const response_or_errort<smt_responset> response_255 =
123+
validate_smt_response(*smt2irep("((a #xff))").parsed_output);
124+
CHECK(
125+
*response_255.get_if_valid() ==
126+
smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
127+
smt_identifier_termt{"a", smt_bit_vector_sortt{8}},
128+
smt_bit_vector_constant_termt{255, 8}}}});
129+
}
130+
SECTION("Binary value")
131+
{
132+
const response_or_errort<smt_responset> response_42 =
133+
validate_smt_response(*smt2irep("((a #b00101010))").parsed_output);
134+
CHECK(
135+
*response_42.get_if_valid() ==
136+
smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
137+
smt_identifier_termt{"a", smt_bit_vector_sortt{8}},
138+
smt_bit_vector_constant_termt{42, 8}}}});
139+
}
134140
}
135141
SECTION("Multiple valuation pairs.")
136142
{

0 commit comments

Comments
 (0)