Version abc80909

1 files changed, 12 insertions, 0 deletions

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 3bdc63f6..aaaa6407 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -54,6 +54,18 @@ struct Ssw_Pars_t_
     int              nIters;        // the number of iterations performed
 };
 
+// sequential counter-example
+typedef struct Ssw_Cex_t_   Ssw_Cex_t;
+struct Ssw_Cex_t_
+{
+    int              iPo;               // the zero-based number of PO, for which verification failed
+    int              iFrame;            // the zero-based number of the time-frame, for which verificaiton failed
+    int              nRegs;             // the number of registers in the miter 
+    int              nPis;              // the number of primary inputs in the miter
+    int              nBits;             // the number of words of bit data used
+    unsigned         pData[0];          // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////