Emit SMT object properties in deterministic order

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -24,8 +24,10 @@
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 
+#include <algorithm>
 #include <stack>
 #include <unordered_set>
+#include <vector>
 
 /// Issues a command to the solving process which is expected to optionally
 /// return a success status followed by the actual response of interest.
@@ -706,18 +708,34 @@ lookup_decision_procedure_result(
 void smt2_incremental_decision_proceduret::define_object_properties()
 {
   object_properties_defined.resize(object_map.size());
+  // The object map is an unordered map, whose iteration order depends on the
+  // hash values of the object base expressions. These hashes may differ
+  // across platforms and toolchains, for example when the signedness of
+  // `char` differs. Establish a deterministic ordering based on the objects'
+  // unique identifiers before emitting the definitions, so that the solver
+  // receives them in a stable order.
+  std::vector<const decision_procedure_objectt *> objects;
+  objects.reserve(object_map.size());
   for(const auto &key_value : object_map)
+    objects.push_back(&key_value.second);
+  std::sort(
+    objects.begin(),
+    objects.end(),
+    [](
+      const decision_procedure_objectt *left,
+      const decision_procedure_objectt *right)
+    { return left->unique_id < right->unique_id; });
+  for(const decision_procedure_objectt *object : objects)
   {
-    const decision_procedure_objectt &object = key_value.second;
-    if(object_properties_defined[object.unique_id])
+    if(object_properties_defined[object->unique_id])
       continue;
     else
-      object_properties_defined[object.unique_id] = true;
-    define_dependent_functions(object.size);
+      object_properties_defined[object->unique_id] = true;
+    define_dependent_functions(object->size);
     solver_process->send(object_size_function.make_definition(
-      object.unique_id, convert_expr_to_smt(object.size)));
+      object->unique_id, convert_expr_to_smt(object->size)));
     solver_process->send(is_dynamic_object_function.make_definition(
-      object.unique_id, object.is_dynamic));
+      object->unique_id, object->is_dynamic));
   }
 }
 

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -480,22 +480,12 @@ TEST_CASE(
     std::vector<smt_commandt> expected_commands{
       smt_declare_function_commandt{foo_term, {}},
       smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
-      invalid_pointer_object_size_definition,
       null_object_size_definition,
       null_object_dynamic_definition,
+      invalid_pointer_object_size_definition,
       invalid_pointer_object_dynamic_definition,
       smt_check_sat_commandt{}};
-    REQUIRE(
-      (test.sent_commands.size() == expected_commands.size() &&
-       std::all_of(
-         expected_commands.begin(),
-         expected_commands.end(),
-         [&](const smt_commandt &command) -> bool {
-           return std::find(
-                    test.sent_commands.begin(),
-                    test.sent_commands.end(),
-                    command) != test.sent_commands.end();
-         })));
+    REQUIRE(test.sent_commands == expected_commands);
     SECTION("Get \"foo\" value back")
     {
       test.sent_commands.clear();