diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 4e47117b3..9dfbd2a25 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -735,6 +735,12 @@ def ywfile_signal(sig, step, mask=None):
 
     output = []
 
+    def ywfile_signal_error(reason, detail=None):
+        msg = f"Yosys witness signal mismatch for {sig.pretty()}: {reason}"
+        if detail:
+            msg += f" ({detail})"
+        raise ValueError(msg)
+
     if sig.path in smt_wires:
         for wire in smt_wires[sig.path]:
             width, offset = wire["width"], wire["offset"]
@@ -765,6 +771,12 @@ def ywfile_signal(sig, step, mask=None):
             for mem in smt_mems[sig.memory_path]:
                 width, size, bv = mem["width"], mem["size"], mem["statebv"]
 
+                if sig.memory_addr is not None and sig.memory_addr >= size:
+                    ywfile_signal_error(
+                        "memory address out of bounds",
+                        f"address={sig.memory_addr} size={size}",
+                    )
+
                 smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"])
 
                 if bv:
@@ -781,18 +793,34 @@ def ywfile_signal(sig, step, mask=None):
                     smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
 
                 output.append((0, sig.width, smt_expr))
+        else:
+            ywfile_signal_error("memory not found in design")
 
     output.sort()
 
     output = [chunk for chunk in output if chunk[0] != chunk[1]]
 
+    if not output:
+        if sig.memory_path:
+            ywfile_signal_error("memory signal has no matching bits in design")
+        else:
+            ywfile_signal_error("signal not found in design")
+
     pos = 0
 
     for start, end, smt_expr in output:
-        assert start == pos
+        if start != pos:
+            ywfile_signal_error(
+                "signal width/offset mismatch",
+                f"expected coverage at bit {pos}",
+            )
         pos = end
 
-    assert pos == sig.width
+    if pos != sig.width:
+        ywfile_signal_error(
+            "signal width/offset mismatch",
+            f"covered {pos} of {sig.width} bits",
+        )
 
     if len(output) == 1:
         return output[0][-1]