Engine heuristic: fix for assumptions unsupported by k-induction

The k-induction engine now correctly reports unsupported assumptions, and is then skipped by the engine selection heuristic. Fixes #921.
diffblue · kroening · Jan 6, 2025 · Jan 7, 2025 · d07c065aae7853f261fdd93fdffa94c9f18d5c51
commit d07c065aae7853f261fdd93fdffa94c9f18d5c51
diff --git a/regression/ebmc/k-induction/k-induction6.desc b/regression/ebmc/k-induction/k-induction6.desc
@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 k-induction6.sv
 
-^EXIT=10$
+^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$
+^\[main\.p0\] always main\.x: PROVED up to bound 5$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The property should hold, but is reported as refuted.
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
@@ -78,9 +78,9 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
         id2string(symbol.location.get_comment());
 
       // Don't try to prove assumption properties.
-      if(symbol.value.id() == ID_sva_assume)
+      if(properties.properties.back().is_assumption())
       {
-        properties.properties.back().status = propertyt::statust::ASSUMED;
+        properties.properties.back().assumed();
         properties.properties.back().normalized_expr =
           normalize_property(to_sva_assume_expr(symbol.value).op());
       }

diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
@@ -103,6 +103,11 @@ class ebmc_propertiest
       return status == statust::INCONCLUSIVE;
     }
 
+    void assumed()
+    {
+      status = statust::ASSUMED;
+    }
+
     void unknown()
     {
       status = statust::UNKNOWN;
@@ -164,6 +169,11 @@ class ebmc_propertiest
     {
       return ::is_exists_path(original_expr);
     }
+
+    bool is_assumption() const
+    {
+      return original_expr.id() == ID_sva_assume;
+    }
   };
 
   typedef std::list<propertyt> propertiest;
@@ -209,11 +219,18 @@ class ebmc_propertiest
     return result;
   }
 
-  void reset_failure_to_unknown()
+  /// Resets properties/assumptions in FAILURE state to
+  /// ASSUMED/UNKNOWN respectively.
+  void reset_failure()
   {
     for(auto &p : properties)
       if(p.is_failure())
-        p.unknown();
+      {
+        if(p.is_assumption())
+          p.assumed();
+        else
+          p.unknown();
+      }
   }
 };
 

diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
@@ -170,10 +170,24 @@ Function: k_inductiont::operator()
 
 void k_inductiont::operator()()
 {
+  // Unsupported assumption?
+  bool assumption_unsupported = false;
+  for(auto &property : properties.properties)
+  {
+    if(!supported(property) && property.is_assumed())
+    {
+      assumption_unsupported = true;
+      property.failure("property unsupported by k-induction");
+    }
+  }
+
+  if(assumption_unsupported)
+    return; // give up
+
   // Fail unsupported properties
   for(auto &property : properties.properties)
   {
-    if(!supported(property))
+    if(!supported(property) && !property.is_assumed())
       property.failure("property unsupported by k-induction");
   }
 

diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
@@ -384,12 +384,13 @@ property_checker_resultt engine_heuristic(
   k_induction(
     1, transition_system, properties, solver_factory, message_handler);
 
-  properties.reset_failure_to_unknown();
+  properties.reset_failure();
 
   if(!properties.has_unknown_property())
     return property_checker_resultt{properties}; // done
 
   // Now try BMC with bound 5, word-level
+  message.status() << "Attempting BMC with bound 5" << messaget::eom;
 
   bmc(
     5,     // bound
@@ -400,7 +401,7 @@ property_checker_resultt engine_heuristic(
     solver_factory,
     message_handler);
 
-  properties.reset_failure_to_unknown();
+  properties.reset_failure();
 
   if(!properties.has_unknown_property())
     return property_checker_resultt{properties}; // done