		Search-engine friendly clone of the ACL2 documentation.

Sd-problem

An alleged problem noticed by skip detection.

This is a product type introduced by defprod.

type — symbolp: What kind of problem this is. At the moment the type is always :skipped and means that we think some wire is suspiciously skipped. But we imagine that we could add other kinds of analysis that look, e.g., for wires that are oddly duplicated, etc., and hence have other types.
priority — natp: A heuristic score that we give to problems to indicate how likely they are to be a real problem. For instance, we assign extra priority to a sequence of wires like foo1, foo2, foo4, foo5 because the skipped wire is in the middle. We also might assign extra priority if one of the other wires is duplicated.
groupsize — natp: Says how many wires had this same pattern. We generally think that the larger the group size is, the more likely the problem is to be legitimate.
key — sd-key: The sd-key-p for the missing wire.
ctx — vl-context1: Says where this problem originates.