Set final status of UNKNOWN properties

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -277,6 +277,22 @@ void update_properties_status_not_checked(
   }
 }
 
+void update_properties_status_unknown(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties)
+{
+  for(auto &property_pair : properties)
+  {
+    if(property_pair.second.status == property_statust::UNKNOWN)
+    {
+      // This could have any status except NOT_CHECKED.
+      // We consider them PASS because we do verification modulo bounds.
+      property_pair.second.status = property_statust::PASS;
+      updated_properties.insert(property_pair.first);
+    }
+  }
+}
+
 void output_coverage_report(
   const std::string &cov_out,
   const abstract_goto_modelt &goto_model,

src/goto-checker/bmc_util.h

@@ -117,6 +117,16 @@ void update_properties_status_not_checked(
   propertiest &properties,
   std::unordered_set<irep_idt> &updated_properties);
 
+/// Sets property status for UNKNOWN properties.
+/// \param [inout] properties: The status is updated in this data structure
+/// \param [inout] updated_properties: The set of property IDs of
+///   updated properties
+/// Note: we currently declare everything PASS that is UNKNOWN at the
+///   end of the model checking algorithm.
+void update_properties_status_unknown(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties);
+
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \