Skip to content

Commit 3e19910

Browse files
committed
sort value set to_predicate subexpressions
1 parent 97c568f commit 3e19910

File tree

2 files changed

+6
-10
lines changed

2 files changed

+6
-10
lines changed

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,7 @@ exprt value_set_abstract_objectt::to_predicate_internal(const exprt &name) const
350350
[&name](const abstract_object_pointert &value) {
351351
return value->to_predicate(name);
352352
});
353+
std::sort(all_predicates.begin(), all_predicates.end());
353354

354355
return or_exprt(all_predicates);
355356
}

unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -70,12 +70,7 @@ SCENARIO(
7070
WHEN("{ 0, 1, 2 }")
7171
{
7272
auto obj = make_value_set({val0, val1, val2}, environment, ns);
73-
auto pred = obj->to_predicate(x_name);
74-
THEN("predicate is x == 0 || x == 1 || x == 2")
75-
{
76-
auto repr = expr_to_str(pred);
77-
REQUIRE(repr == "x == 0 || x == 1 || x == 2");
78-
}
73+
THEN_PREDICATE(obj, "x == 0 || x == 1 || x == 2");
7974
}
8075
WHEN("{ [0, 1] }")
8176
{
@@ -85,17 +80,17 @@ SCENARIO(
8580
WHEN("{ [0, 1], 2 }")
8681
{
8782
auto obj = make_value_set({interval_0_1, val2}, environment, ns);
88-
THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2");
83+
THEN_PREDICATE(obj, "x == 2 || 0 <= x && x <= 1");
8984
}
9085
WHEN("{ [0, 1], 2, 3 }")
9186
{
9287
auto obj = make_value_set({interval_0_1, val2, val3}, environment, ns);
93-
THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 3 || x == 2");
88+
THEN_PREDICATE(obj, "x == 2 || x == 3 || 0 <= x && x <= 1");
9489
}
9590
WHEN("{ [0, 1], 1, 2 }")
9691
{
9792
auto obj = make_value_set({interval_0_1, val1, val2}, environment, ns);
98-
THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2");
93+
THEN_PREDICATE(obj, "x == 2 || 0 <= x && x <= 1");
9994
}
10095
WHEN("{ [0, 1], [1, 2] }")
10196
{
@@ -110,7 +105,7 @@ SCENARIO(
110105
WHEN("{ [0, 1], [2, 3] }")
111106
{
112107
auto obj = make_value_set({interval_0_1, interval_2_3}, environment, ns);
113-
THEN_PREDICATE(obj, "2 <= x && x <= 3 || 0 <= x && x <= 1");
108+
THEN_PREDICATE(obj, "0 <= x && x <= 1 || 2 <= x && x <= 3");
114109
}
115110
}
116111
}

0 commit comments

Comments
 (0)