Skip to content

Commit fc274db

Browse files
committed
Ensure result of to_predicates is deterministic
The order of entries in an unordered map would previously yield varying results. This caused spurious unit test failures as unit tests perform exact string matching on the output.
1 parent f0a4e75 commit fc274db

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,11 @@
99
#include <analyses/variable-sensitivity/abstract_environment.h>
1010
#include <analyses/variable-sensitivity/abstract_object_statistics.h>
1111
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
12+
1213
#include <util/expr_util.h>
1314
#include <util/simplify_expr.h>
1415
#include <util/simplify_expr_class.h>
16+
#include <util/simplify_utils.h>
1517

1618
#include <algorithm>
1719
#include <map>
@@ -427,7 +429,7 @@ exprt abstract_environmentt::to_predicate() const
427429
if(is_top())
428430
return true_exprt();
429431

430-
auto predicates = std::vector<exprt>{};
432+
exprt::operandst predicates;
431433
for(const auto &entry : map.get_view())
432434
{
433435
auto sym = entry.first;
@@ -439,6 +441,8 @@ exprt abstract_environmentt::to_predicate() const
439441

440442
if(predicates.size() == 1)
441443
return predicates.front();
444+
445+
sort_operands(predicates);
442446
return and_exprt(predicates);
443447
}
444448

0 commit comments

Comments
 (0)