Use NOT_CHECKED when checking status

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

Author: FrNecas

src/2ls/2ls_parse_options.cpp

@@ -1249,7 +1249,8 @@ void twols_parse_optionst::report_properties(
         it!=property_map.end();
         it++)
     {
-      if(it->second.status==property_statust::UNKNOWN)
+      if(it->second.status==property_statust::UNKNOWN ||
+         it->second.status==property_statust::NOT_CHECKED)
         unknown++;
       if(it->second.status==property_statust::FAIL)
         failed++;

src/2ls/cover_goals_ext.cpp

@@ -130,7 +130,8 @@ void cover_goals_extt::assignment()
     for(goal_mapt::const_iterator it=goal_map.begin();
         it!=goal_map.end(); it++, g_it++)
     {
-      if(property_map.at(it->first).status==property_statust::UNKNOWN &&
+      if((property_map.at(it->first).status==property_statust::UNKNOWN ||
+          property_map.at(it->first).status==property_statust::NOT_CHECKED) &&
          solver.l_get(g_it->condition).is_true())
       {
         property_map.at(it->first).status=property_statust::FAIL;
@@ -159,7 +160,8 @@ void cover_goals_extt::assignment()
     for(goal_mapt::const_iterator it=goal_map.begin();
         it!=goal_map.end(); it++, g_it++)
     {
-      if(property_map.at(it->first).status==property_statust::UNKNOWN &&
+      if((property_map.at(it->first).status==property_statust::UNKNOWN ||
+          property_map.at(it->first).status==property_statust::NOT_CHECKED) &&
          solver.l_get(g_it->condition).is_true())
       {
         property_map.at(it->first).status=property_statust::FAIL;

src/2ls/summary_checker_base.cpp

@@ -148,7 +148,8 @@ resultt summary_checker_baset::check_properties()
   {
     if(p_it->second.status==property_statust::FAIL)
       return resultt::FAIL;
-    if(p_it->second.status==property_statust::UNKNOWN)
+    if(p_it->second.status==property_statust::UNKNOWN ||
+      p_it->second.status==property_statust::NOT_CHECKED)
       result=resultt::UNKNOWN;
   }
 
@@ -238,7 +239,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::UNKNOWN)
+    if(property_map.at(property_id).status!=property_statust::NOT_CHECKED)
       continue;
 
     // TODO: some properties do not show up in initialize_property_map

src/2ls/summary_checker_nonterm.cpp

@@ -589,7 +589,8 @@ resultt summary_checker_nontermt::check_nonterm_linear()
   {
     if(p_it->second.status==property_statust::FAIL)
       return resultt::FAIL;
-    if(p_it->second.status==property_statust::UNKNOWN)
+    if(p_it->second.status==property_statust::UNKNOWN ||
+      p_it->second.status==property_statust::NOT_CHECKED)
       result=resultt::UNKNOWN;
   }