Adding features for invariant minimization.

7 files changed, 625 insertions, 104 deletions

diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 05cb09c1..9647d020 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -95,8 +95,6 @@ void        Abc_FrameSetStatus( int Status )                 { ABC_FREE( s_Globa
 void        Abc_FrameSetManDsd( void * pMan )                { if (s_GlobalFrame->pManDsd  && s_GlobalFrame->pManDsd  != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd,  0); s_GlobalFrame->pManDsd = pMan;  }
 void        Abc_FrameSetManDsd2( void * pMan )               { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; }
 void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
-void        Abc_FrameSetCnf( Vec_Int_t * vCnf )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
-void        Abc_FrameSetStr( Vec_Str_t * vStr )              { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
 void        Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs )        { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
 void        Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs )        { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
 
@@ -227,8 +225,6 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     ABC_FREE( p->pCex2 );
     ABC_FREE( p->pCex );
     Vec_IntFreeP( &p->pAbcWlcInv );
-    Vec_IntFreeP( &p->pAbcWlcCnf );
-    Vec_StrFreeP( &p->pAbcWlcStr );
     Abc_NamDeref( s_GlobalFrame->pJsonStrs );
     Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );    
     ABC_FREE( p );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index ff59b81a..278a9191 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -129,8 +129,6 @@ struct Abc_Frame_t_
     void *          pAbc85Delay;
     void *          pAbcWlc;
     Vec_Int_t *     pAbcWlcInv;
-    Vec_Int_t *     pAbcWlcCnf;
-    Vec_Str_t *     pAbcWlcStr;
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 0bf27f7b..1a98fb71 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
 {
     Wlc_Obj_t * pObj;
     int i, k, nNum, nRange, nBits = 0;
@@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         nRange = Wlc_ObjRange(pObj);
         for ( k = 0; k < nRange; k++ )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
+            nNum = Vec_IntEntry(vCounts, nBits + k);
             if ( nNum )
                 break;
         }
@@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
         for ( k = 0; k < nRange; k++ )
         {
-            nNum = Vec_IntEntry( vInv, nBits + k );
+            nNum = Vec_IntEntry( vCounts, nBits + k );
             if ( nNum == 0 )
                 continue;
             printf( "  [%d] -> %d", k, nNum );
@@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         printf( "\n");
         nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( Vec_IntSize(vCounts) == nBits );
 }
 
 /**Function*************************************************************
@@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
 {
+    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
+    extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
+
+    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+    Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
+
     Wlc_Obj_t * pObj;
     int i, k, nNum, nRange, nBits = 0;
     Abc_Ntk_t * pMainNtk = NULL;
@@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     // start the network
     pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     // duplicate the name and the spec
-    pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+    pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
     // create primary inputs
-    Wlc_NtkForEachCi( pNtk, pObj, i )
+    if ( pNtk == NULL )
     {
-        if ( pObj->Type != WLC_OBJ_FO )
-            continue;
-        nRange = Wlc_ObjRange(pObj);
-        for ( k = 0; k < nRange; k++ )
+        int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+        Vec_IntForEachEntry( vCounts, Entry, i )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
-            if ( nNum )
-                break;
+            if ( Entry == 0 )
+                continue;
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "pi%d", i );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
         }
-        if ( k == nRange )
+        if ( Abc_NtkPiNum(pMainNtk) != nInputs )
         {
-            nBits += nRange;
-            continue;
+            printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+            Abc_NtkDelete( pMainNtk );
+            return NULL;
         }
-        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
-        for ( k = 0; k < nRange; k++ )
+    }
+    else
+    {
+        Wlc_NtkForEachCi( pNtk, pObj, i )
         {
-            nNum = Vec_IntEntry( vInv, nBits + k );
-            if ( nNum == 0 )
+            if ( pObj->Type != WLC_OBJ_FO )
                 continue;
-            //printf( "  [%d] -> %d", k, nNum );
-            pMainObj = Abc_NtkCreatePi( pMainNtk );
-            sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
-            Abc_ObjAssignName( pMainObj, Buffer, NULL );
-
+            nRange = Wlc_ObjRange(pObj);
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry(vCounts, nBits + k);
+                if ( nNum )
+                    break;
+            }
+            if ( k == nRange )
+            {
+                nBits += nRange;
+                continue;
+            }
+            //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry( vCounts, nBits + k );
+                if ( nNum == 0 )
+                    continue;
+                //printf( "  [%d] -> %d", k, nNum );
+                pMainObj = Abc_NtkCreatePi( pMainNtk );
+                sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+                Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+            }
+            //printf( "\n");
+            nBits += nRange;
         }
-        //printf( "\n");
-        nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
     // create node
     pMainObj = Abc_NtkCreateNode( pMainNtk );
     Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
         Abc_ObjAddFanin( pMainObj, pMainTemp );
     pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+    Vec_IntFree( vCounts );
+    Vec_StrFree( vSop );
     // create PO
     pMainTemp = Abc_NtkCreatePo( pMainNtk );
     Abc_ObjAddFanin( pMainTemp, pMainObj );
@@ -145,6 +174,66 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     return pMainNtk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Translate current network into an interpolant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
+{
+    Vec_Int_t * vRes = NULL;
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+        printf( "The number of outputs is other than 1.\n" );
+    else if ( Abc_NtkNodeNum(pNtk) != 1 )
+        printf( "The number of internal nodes is other than 1.\n" );
+    else
+    {
+        Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+        char * pName, * pCube, * pSop = (char *)pNode->pData;
+        Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+        Abc_Obj_t * pFanin; int i, k, Value, nLits;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            assert( Abc_ObjIsCi(pFanin) );
+            pName = Abc_ObjName(pFanin);
+            for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+                if ( pName[k] < '0' || pName[k] > '9' )
+                    break;
+            if ( k == (int)strlen(pName)-1 )
+            {
+                printf( "Cannot read input name of fanin %d.\n", i );
+                Value = i;
+            }
+            else 
+                Value = atoi(pName + k + 1);
+            Vec_IntPush( vFanins, Value );
+        }
+        assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
+        vRes = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
+        Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
+        {
+            nLits = 0;
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    nLits++;
+            Vec_IntPush( vRes, nLits );
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
+        }
+        Vec_IntPush( vRes, nRegs );
+        Vec_IntFree( vFanins );
+    }
+    return vRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index f3eb6dd7..93614938 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -32,18 +32,21 @@ static int  Abc_CommandReadWlc  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandPsInv    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandGetInv   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandProfile  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int  Abc_CommandInvPs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvGet   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvMin   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
 
 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcInv;                                }
-static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcCnf;                                }
-static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcStr;                                }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -66,10 +69,15 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%write",      Abc_CommandWriteWlc,  0 );
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%psinv",      Abc_CommandPsInv,     0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%getinv",     Abc_CommandGetInv,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",    Abc_CommandProfile,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
+
+    Cmd_CommandAdd( pAbc, "Word level", "inv_ps",      Abc_CommandInvPs,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_print",   Abc_CommandInvPrint,  0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_check",   Abc_CommandInvCheck,  0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_get",     Abc_CommandInvGet,    0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_put",     Abc_CommandInvPut,    0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_min",     Abc_CommandInvMin,    0 );
 }
 
 /**Function********************************************************************
@@ -440,10 +448,108 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+        return 0;
+    }
+    Wlc_WinProfileArith( pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%profile [-vh]\n" );
+    Abc_Print( -2, "\t         profiles arithmetic components in the word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+        return 0;
+    }
+    // transform
+    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //Wlc_GenerateSmtStdout( pAbc );
+    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
+    pNtk = Wlc_NtkDupSingleNodes( pNtk );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
     extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Vec_Int_t * vCounts;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -461,24 +567,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" );
         return 0;
     }
-    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
         return 0;
     }
+    vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
+    Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
+    Vec_IntFree( vCounts );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: inv_ps [-vh]\n" );
+    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Pdr_InvPrint( Vec_Int_t * vInv );
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
     if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
         return 0;
     }
-    Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
+    Pdr_InvPrint( Wlc_AbcGetInv(pAbc) );
     return 0;
-    usage:
-    Abc_Print( -2, "usage: %%psinv [-vh]\n" );
-    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+usage:
+    Abc_Print( -2, "usage: inv_print [-vh]\n" );
+    Abc_Print( -2, "\t         prints the current inductive invariant\n" );
     Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -496,11 +644,9 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
-    Abc_Ntk_t * pMainNtk;
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -516,28 +662,76 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
         return 0;
     }
-    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
         return 0;
     }
+    Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc)  );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: inv_check [-vh]\n" );
+    Abc_Print( -2, "\t         checks that the invariant is indeed an inductive invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+    Abc_Ntk_t * pMainNtk;
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
     if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+        Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
         return 0;
     }
     // derive the network
-    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+    if ( pMainNtk )
+        Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
     return 0;
-    usage:
-    Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+usage:
+    Abc_Print( -2, "usage: inv_get [-vh]\n" );
     Abc_Print( -2, "\t         places invariant found by PDR as the current network in the main-space\n" );
     Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -556,34 +750,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs );
+    Vec_Int_t * vInv = NULL;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
         }
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" );
         return 0;
     }
-    Wlc_WinProfileArith( pNtk );
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
+        return 0;
+    }
+    // derive the network
+    vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) );
+    if ( vInv )
+        Abc_FrameSetInv( vInv );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%profile [-vh]\n" );
-    Abc_Print( -2, "\t         profiles arithmetic components in the word-level networks\n" );
+    Abc_Print( -2, "usage: inv_put [-vh]\n" );
+    Abc_Print( -2, "\t         inputs the current network in the main-space as an invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -600,42 +805,49 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv );
+    Vec_Int_t * vInv, * vInv2;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( pAbc->pGia == NULL )
     {
-        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
         return 0;
     }
-    // transform
-    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
-    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
-    //Wlc_AbcUpdateNtk( pAbc, pNtk );
-    //Wlc_GenerateSmtStdout( pAbc );
-    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
-    pNtk = Wlc_NtkDupSingleNodes( pNtk );
-    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
+        return 0;
+    }
+    vInv = Wlc_AbcGetInv(pAbc);
+    if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
+        return 0;
+    }
+    vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
+    if ( vInv2 )
+        Abc_FrameSetInv( vInv2 );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%test [-vh]\n" );
-    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "usage: inv_min [-vh]\n" );
+    Abc_Print( -2, "\t         minimizes the number of clauses in the current invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 66cae36e..c625e366 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -923,9 +923,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     if ( p->pPars->fDumpInv )
     {
         char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
-        Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
-        Abc_FrameSetStr( Pdr_ManDumpString(p) );
-        Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
+        Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
         Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
     }
     p->tTotal += Abc_Clock() - clk;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 02b90a36..f29b792c 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -605,9 +605,237 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
     //Vec_PtrFree( vCubes );
     Vec_PtrFreeP( &p->vInfCubes );
     p->vInfCubes = vCubes;
+    Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
     return vResult;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Remove clauses while maintaining the invariant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
+{
+    int i, k = 0, Count;
+    Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
+    Vec_IntForEachEntry( vCounts, Count, i )
+        if ( Count )
+            Vec_IntWriteEntry( vMap, i, k++ );
+    return vMap;
+}
+Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
+{
+    int i, k, * pCube, * pList = Vec_IntArray(vInv);
+    Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
+    Pdr_ForEachCube( pList, pCube, i )
+        for ( k = 0; k < pCube[0]; k++ )
+            Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
+    return vCounts;
+}
+int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
+{
+    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+    int nZeros = Vec_IntCountZero( vCounts );
+    Vec_IntFree( vCounts );
+    return Vec_IntEntryLast(vInv) - nZeros;
+}
+
+Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
+{
+    Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
+    Vec_Int_t * vMap = Pdr_InvMap( vCounts );
+    int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
+    int i, k, * pCube, * pList = Vec_IntArray(vInv);
+    char * pBuffer = ABC_ALLOC( char, nVars );
+    for ( i = 0; i < nVars; i++ )
+        pBuffer[i] = '-';
+    Pdr_ForEachCube( pList, pCube, i )
+    {
+        for ( k = 0; k < pCube[0]; k++ )
+            pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
+        for ( k = 0; k < nVars; k++ )
+            Vec_StrPush( vStr, pBuffer[k] );
+        Vec_StrPush( vStr, ' ' );
+        Vec_StrPush( vStr, '1' );
+        Vec_StrPush( vStr, '\n' );
+        for ( k = 0; k < pCube[0]; k++ )
+            pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
+    }
+    Vec_StrPush( vStr, '\0' );
+    ABC_FREE( pBuffer );
+    Vec_IntFree( vMap );
+    return vStr;
+}
+void Pdr_InvPrint( Vec_Int_t * vInv )
+{
+    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+    Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
+    printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
+    printf( "%s", Vec_StrArray( vStr ) );
+    Vec_IntFree( vCounts );
+    Vec_StrFree( vStr );
+}
+
+void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
+{
+    int nBTLimit = 0;
+    int i, k, status, nFailed = 0; 
+    // create SAT solver
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // collect cubes
+    int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
+    // create variables
+    Vec_Int_t * vLits = Vec_IntAlloc(100);
+    int nVars = Gia_ManRegNum(p);
+    int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
+    int iFiVarBeg = 1 + Gia_ManPoNum(p);
+    assert( Gia_ManPoNum(p) == 1 );
+    // add cubes
+    Pdr_ForEachCube( pList, pCube, i )
+    {
+        // collect literals
+        Vec_IntClear( vLits );
+        for ( k = 0; k < pCube[0]; k++ )
+            Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+        // add it to the solver
+        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+        assert( status == 1 );
+    }
+    // iterate through cubes in the direct order
+    Pdr_ForEachCube( pList, pCube, i )
+    {
+        // collect cube
+        Vec_IntClear( vLits );
+        for ( k = 0; k < pCube[0]; k++ )
+           Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+        // check if this cube intersects with the complement of other cubes in the solver
+        // if it does not intersect, then it is redundant and can be skipped
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef ) // timeout
+            break;
+        if ( status == l_False ) // unsat -- correct
+            continue;
+        assert( status == l_True );
+        nFailed++;
+    }
+    if ( nFailed )
+        printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, nCubes );
+    else
+        printf( "Invariant verification passes.\n" );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    Vec_IntFree( vLits );
+}
+
+Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
+{
+    int nBTLimit = 0;
+    int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; 
+    Vec_Int_t * vRes = NULL;
+    // create SAT solver
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
+    // create variables
+    Vec_Int_t * vLits = Vec_IntAlloc(100);
+    Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
+    int nVars = Gia_ManRegNum(p);
+    int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
+    int iFiVarBeg = 1 + Gia_ManPoNum(p);
+    int iAuxVarBeg = sat_solver_nvars(pSat);
+    assert( Gia_ManPoNum(p) == 1 );
+    // allocate auxiliary variables
+    sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
+    // add clauses
+    Pdr_ForEachCube( pList, pCube, i )
+    {
+        // collect literals
+        Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
+        for ( k = 0; k < pCube[0]; k++ )
+            Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+        // add it to the solver
+        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+        assert( status == 1 );
+    }
+    // iterate through clauses 
+    Pdr_ForEachCube( pList, pCube, i )
+    {
+        if ( Vec_BitEntry(vRemoved, i) )
+            continue;
+        // collect aux literals for remaining clauses
+        Vec_IntClear( vLits );
+        for ( k = 0; k < nCubes; k++ )
+            if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
+                Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
+        nLits = Vec_IntSize( vLits );
+        // try removing other clauses
+        fCannot = 0;
+        Pdr_ForEachCube( pList, pCube, n )
+        {
+            if ( Vec_BitEntry(vRemoved, n) || n == i )
+                continue;
+            // collect cube
+            Vec_IntShrink( vLits, nLits );
+            for ( k = 0; k < pCube[0]; k++ )
+               Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+            // check if this cube intersects with the complement of other cubes in the solver
+            // if it does not intersect, then it is redundant and can be skipped
+            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+            if ( status == l_Undef ) // timeout
+            {
+                fFailed = 1;
+                break;
+            }
+            if ( status == l_False ) // unsat -- correct
+                continue;
+            assert( status == l_True );
+            // cannot remove
+            fCannot = 1;
+            break;
+        }
+        if ( fFailed )
+            break;
+        if ( fCannot )
+            continue;
+        printf( "Removing clause %d.\n", i );
+        Vec_BitWriteEntry( vRemoved, i, 1 );
+        nRemoved++;
+    }
+    if ( nRemoved )
+        printf( "Invariant minimization reduced %d clauses (out of %d).\n", nRemoved, nCubes );
+    else
+        printf( "Invariant minimization did not change the invariant.\n" ); 
+    // cleanup cover
+    if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
+    {
+        vRes = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vRes, nCubes-nRemoved );
+        Pdr_ForEachCube( pList, pCube, i )
+            if ( !Vec_BitEntry(vRemoved, i) )
+                for ( k = 0; k <= pCube[0]; k++ )
+                    Vec_IntPush( vRes, pCube[k] );
+        Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
+    }
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    Vec_BitFree( vRemoved );
+    Vec_IntFree( vLits );
+    return vRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 53a8a54a..32e97772 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -284,7 +284,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
     }
     Vec_StrPushBuffer( vStr, pBuff, k );
     Vec_StrPush( vStr, ' ' );
-    Vec_StrPush( vStr, '0' );
+    Vec_StrPush( vStr, '1' );
     Vec_StrPush( vStr, '\n' );
     ABC_FREE( pBuff );
 }