Initialize properties with UNKNOWN

This is better for backwards compatibility for now, since we have no way
of checking if a property was checked or we simply could not check it.
However this is a potential place for improvements.

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/2ls/summary_checker_ai.cpp

@@ -31,6 +31,7 @@ resultt summary_checker_ait::operator()(
 
   // properties
   property_map=initialize_properties(goto_model);
+  set_properties_unknown();
 
   resultt result=resultt::UNKNOWN;
   bool finished=false;

src/2ls/summary_checker_base.cpp

@@ -70,6 +70,7 @@ void summary_checker_baset::SSA_functions(
 
   // properties
   property_map=initialize_properties(goto_model);
+  set_properties_unknown();
 }
 
 void summary_checker_baset::summarize(
@@ -239,7 +240,7 @@ void summary_checker_baset::check_properties(
     }
 
     // do not recheck properties that have already been decided
-    if(property_map.at(property_id).status!=property_statust::NOT_CHECKED)
+    if(property_map.at(property_id).status!=property_statust::UNKNOWN)
       continue;
 
     // TODO: some properties do not show up in initialize_property_map

src/2ls/summary_checker_base.h

@@ -116,6 +116,17 @@ class summary_checker_baset:public messaget
     const exprt::operandst& loophead_selects,
     incremental_solvert&);
 
+  // FIXME: This is a backwards-compatible hack. CPROVER introduced property
+  //        status NOT_CHECKED (previously there was only UNKNOWN). Adjust
+  //        2LS to also differentiate between unknown properties and properties
+  //        that were not checked at all.
+  inline void set_properties_unknown()
+  {
+    for(auto &property : property_map)
+      if(property.second.status==property_statust::NOT_CHECKED)
+        property.second.status=property_statust::UNKNOWN;
+  }
+
   friend graphml_witness_extt;
 };