From 2aa8d266ad09ba0cbfa8bcf7cd16e6da4e8357f6 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 8 Jul 2025 15:47:33 +1200
Subject: [PATCH] Update unknown covers as well as asserts

Currently only applicable to smtbmc.
Also don't update assert depth during `cover` mode.
---
 sbysrc/sby_core.py          | 7 +++++--
 sbysrc/sby_engine_smtbmc.py | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index d3ed77c..0d4adef 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1260,9 +1260,12 @@ class SbyTask(SbyConfig):
         self.status = "ERROR"
         self.terminate()
 
-    def update_unknown_asserts(self, data):
+    def update_unknown_props(self, data):
         for prop in self.design.hierarchy:
-            if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
+            if prop.status != "UNKNOWN":
+                continue
+            if ((prop.type == prop.Type.ASSERT and self.opt_mode in ["bmc", "prove"]) or
+                (prop.type == prop.Type.COVER and self.opt_mode == "cover")):
                 self.status_db.set_task_property_status(prop, data=data)
 
     def pass_unknown_asserts(self, data):
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index cdd579a..0364929 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -221,7 +221,7 @@ def run(mode, task, engine_idx, engine):
             last_step = current_step
             current_step = int(match[1])
             if current_step != last_step and last_step is not None:
-                task.update_unknown_asserts(dict(source="smtbmc", engine=f"engine_{engine_idx}", step=last_step))
+                task.update_unknown_props(dict(source="smtbmc", engine=f"engine_{engine_idx}", step=last_step))
             return line
 
         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)