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.

Author: tautschnig

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -9,9 +9,11 @@
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <analyses/variable-sensitivity/abstract_object_statistics.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+
 #include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <util/simplify_expr_class.h>
+#include <util/simplify_utils.h>
 
 #include <algorithm>
 #include <map>
@@ -427,7 +429,7 @@ exprt abstract_environmentt::to_predicate() const
   if(is_top())
     return true_exprt();
 
-  auto predicates = std::vector<exprt>{};
+  exprt::operandst predicates;
   for(const auto &entry : map.get_view())
   {
     auto sym = entry.first;
@@ -439,6 +441,8 @@ exprt abstract_environmentt::to_predicate() const
 
   if(predicates.size() == 1)
     return predicates.front();
+
+  sort_operands(predicates);
   return and_exprt(predicates);
 }
 

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

@@ -67,7 +67,7 @@ SCENARIO(
       env.assign(x_name, val2, ns);
       env.assign(y_name, val3, ns);
 
-      THEN_PREDICATE(env, "y == 3 && x == 2");
+      THEN_PREDICATE(env, "x == 2 && y == 3");
     }
   }
 }