Adding new command &mprove for proving groups of properties.

9 files changed, 240 insertions, 26 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index ed38806e..d9d885e3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -372,6 +372,9 @@ static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) {
 static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1;          }
 static inline int          Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
 
+static inline int          Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex )    { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
+static inline int          Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex )    { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
+
 static inline Gia_Obj_t *  Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) );                              }
 
 static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 5288bf35..cb97e0bf 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1393,6 +1393,95 @@ void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues )
         pObj->Value = Vec_IntEntry(vValues, i);
 }
 
+
+#include "base/main/mainInt.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Proving multi-output properties.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
+{
+    Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
+    Gia_Man_t * p = Gia_ManDup( pInit );
+    Gia_Man_t * pGroup;
+    Vec_Int_t * vOuts;
+    Vec_Int_t * vOutMap;
+    Vec_Ptr_t * vCexes;
+    int i, k, nGroupCur, nGroups;
+    clock_t clk, timeComm = 0;
+    clock_t timeStart = clock();
+    // pre-conditions
+    assert( nGroupSize > 0 );
+    assert( pCommLine != NULL );
+    assert( p->nConstrs == 0 );
+    Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine );
+    // create output map
+    vOuts   = Vec_IntStartNatural( Gia_ManPoNum(p) );
+    vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) );
+    vCexes  = Vec_PtrAlloc( Gia_ManPoNum(p) );
+    nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0);
+    for ( i = 0; i < nGroups; i++ )
+    {
+        // derive the group
+        nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize;
+        pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 );
+        Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur );
+        // set the current GIA
+        Abc_FrameUpdateGia( pAbc, pGroup );
+        // solve the group
+        clk = clock();
+        Cmd_CommandExecute( pAbc, pCommLine );
+        timeComm += clock() - clk;
+        // get the solution status
+        if ( nGroupSize == 1 )
+        {
+            Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) );
+            Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) );
+        }
+        else // if ( nGroupSize > 1 )  
+        {
+            Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc );
+            Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc );
+            assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr"
+            assert( vCexesCur != NULL );
+            for ( k = 0; k < nGroupCur; k++ )
+            {
+                Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) );
+                Vec_PtrPush( vCexes, Vec_PtrEntry(vCexesCur, k) );
+            }
+        }
+    }
+    assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) );
+    assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) );
+    // set CEXes
+    if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) )
+        Abc_FrameReplaceCexVec( pAbc, &vCexes );
+    else  // there is no CEXes
+        Vec_PtrFree( vCexes );
+    // report the result
+    Abc_Print( 1, "SUMMARY:  " );
+    Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) );
+    Abc_Print( 1, "UNSAT = %6d. ",      Vec_IntCountEntry(vOutMap, 1) );
+    Abc_Print( 1, "SAT = %6d. ",        Vec_IntCountEntry(vOutMap, 0) );
+    Abc_Print( 1, "UNDEC = %6d. ",      Vec_IntCountEntry(vOutMap, -1) );
+    Abc_Print( 1, "\n" );
+    Abc_PrintTime( 1, "Command time", timeComm );
+    Abc_PrintTime( 1, "Total time  ", clock() - timeStart );
+    // cleanup
+    Vec_IntFree( vOuts );
+    Gia_ManStop( p );
+    return vOutMap;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6da8b17c..a30a2e55 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -382,6 +382,7 @@ static int Abc_CommandAbc9CexInfo            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Cycle              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cone               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -474,7 +475,6 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
 ***********************************************************************/
 void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
 {
-    // update the array vector
     if ( pAbc->vPoEquivs )
         Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs );
     pAbc->vPoEquivs = *pvPoEquivs;
@@ -492,6 +492,51 @@ void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses )
+{
+    if ( pAbc->vStatuses )
+        Vec_IntFree( pAbc->vStatuses );
+    pAbc->vStatuses = *pvStatuses;
+    *pvStatuses = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives array of statuses from the array of CEXes.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes )
+{
+    Vec_Int_t * vStatuses;
+    Abc_Cex_t * pCex;
+    int i;
+    if ( vCexes == NULL )
+        return NULL;
+    vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
+    Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
+    Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
+        if ( pCex != NULL )
+            Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
+    return vStatuses;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_FrameClearDesign()
 {
 }
@@ -882,6 +927,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&cycle",        Abc_CommandAbc9Cycle,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cone",         Abc_CommandAbc9Cone,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -21194,6 +21240,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     Saig_ParBmc_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
     Vec_Ptr_t * vSeqModelVec = NULL;
+    Vec_Int_t * vStatuses = NULL;
     char * pLogFileName = NULL;
     int fOrDecomp = 0;
     int c;
@@ -21356,7 +21403,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
-    pAbc->nFrames = pPars->iFrame;
+    pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
         Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
@@ -21380,11 +21427,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
     }
-    if ( vSeqModelVec )
-    {
-        Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
-        pAbc->nFrames = -1;
-    }
+    vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec );
+    Abc_FrameReplacePoStatuses( pAbc, &vStatuses );        
+    Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
     return 0;
 
 usage:
@@ -22929,14 +22974,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // run the procedure
     pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars );
-    pAbc->nFrames = pPars->iFrame;
+    pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
-    if ( pNtk->vSeqModelVec )
-    {
-        Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
-        pAbc->nFrames = -1;
-    }
-    ABC_FREE( pPars->pOutMap ); // cleanup after PDR
+    Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+    Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
     return 0;
 
 usage:
@@ -30470,6 +30511,75 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
+    Vec_Int_t * vStatus;
+    char * pCommLine = NULL;
+    int c, nGroupSize = 1, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "GSvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nGroupSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nGroupSize <= 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pCommLine = argv[globalUtilOptind];
+            globalUtilOptind++;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
+        return 1;
+    }
+    vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
+    Vec_IntFree( vStatus );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" );
+    Abc_Print( -2, "\t         proves multi-output testcase by splitting outputs into groups\n" );
+    Abc_Print( -2, "\t         (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" );
+    Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize );
+    Abc_Print( -2, "\t-S str : the command line to be executed for each group [default = %s]\n", pCommLine ? pCommLine : "none" );
+    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*************************************************************
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 34678479..722f5465 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -116,6 +116,7 @@ extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );
 extern ABC_DLL Abc_Cex_t *     Abc_FrameReadCex( Abc_Frame_t * p );              
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexVec( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadPoEquivs( Abc_Frame_t * p );  
+extern ABC_DLL Vec_Int_t *     Abc_FrameReadPoStatuses( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Int_t *     Abc_FrameReadObjIds( Abc_Frame_t * p );
 
 extern ABC_DLL int             Abc_FrameReadCexPiNum( Abc_Frame_t * p );              
@@ -138,6 +139,11 @@ extern ABC_DLL void            Abc_FrameSetStatus( int Status );
 
 extern ABC_DLL int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 
+extern ABC_DLL void            Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex );
+extern ABC_DLL void            Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec );
+extern ABC_DLL void            Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs );
+extern ABC_DLL void            Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses );
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index a525afb6..035a8df3 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -65,6 +65,7 @@ int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFr
 Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
 Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p )           { return s_GlobalFrame->vCexVec;      }        
 Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p )         { return s_GlobalFrame->vPoEquivs;    }        
+Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p )       { return s_GlobalFrame->vStatuses;    }        
 Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p )           { return s_GlobalFrame->vAbcObjIds;   }        
        
 int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;   }               
@@ -177,6 +178,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     if ( p->vAbcObjIds)  Vec_IntFree( p->vAbcObjIds );
     if ( p->vCexVec   )  Vec_PtrFreeFree( p->vCexVec );
     if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
+    if ( p->vStatuses )  Vec_IntFree( p->vStatuses );
     if ( p->pLibVer   )  Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
     if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
     if ( p->dd        )  Extra_StopManager( p->dd );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 2d5bf4c8..acd8bbd3 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -101,6 +101,7 @@ struct Abc_Frame_t_
     Abc_Cex_t *     pCex2;         // copy of the above
     Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails
     Vec_Ptr_t *     vPoEquivs;     // equivalence classes of isomorphic primary outputs
+    Vec_Int_t *     vStatuses;     // problem status for each output
     Vec_Int_t *     vAbcObjIds;    // object IDs
     int             Status;                // the status of verification problem (proved=1, disproved=0, undecided=-1)
     int             nFrames;               // the number of time frames completed by BMC
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 97a71512..10d2af3b 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -67,7 +67,7 @@ struct Pdr_Par_t_
     int(*pFuncStop)(int); // callback to terminate
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
     clock_t timeLastSolved; // the time when the last output was solved
-    int * pOutMap;        // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
+    Vec_Int_t * vOutMap;  // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index afcb45b4..f2ba7ba6 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -592,7 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     return 0; // SAT
                 }
                 p->pPars->nFailOuts++;
-                if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
+                if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                     nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                 if ( p->vCexes == NULL )
@@ -684,7 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
-                        if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
+                        if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                         if ( p->vCexes == NULL )
                             p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
@@ -719,7 +719,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL )
                 {
                     p->pPars->nDropOuts++;
-                    if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1;
+                    if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
 //                    printf( "Dropping output %d.\n", p->iOutCur );
                 }
             }
@@ -765,10 +765,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             // count the number of UNSAT outputs
             p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
             // convert previously 'unknown' into 'unsat'
-            if ( p->pPars->pOutMap )
+            if ( p->pPars->vOutMap )
                 for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
-                    if ( p->pPars->pOutMap[k] == -2 ) // unknown
-                        p->pPars->pOutMap[k] = 1; // unsat
+                    if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
+                        Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
             return p->vCexes ? 0 : 1; // UNSAT
         }
         if ( p->pPars->fVerbose ) 
@@ -836,7 +836,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
 {
     Pdr_Man_t * p;
-    int RetValue;
+    int k, RetValue;
     clock_t clk = clock();
     if ( pPars->nTimeOutOne )
         pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
@@ -871,6 +871,11 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     p->tTotal += clock() - clk;
     Pdr_ManStop( p );
     pPars->iFrame--;
+    // convert all -2 (unknown) entries into -1 (undec)
+    if ( pPars->vOutMap )
+        for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
+            if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
+                Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
     return RetValue;
 }
 
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index ef930beb..36a62029 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -83,10 +83,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     }
     if ( pPars->fSolveAll )
     {
-        int i;
-        pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) );
-        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
-            pPars->pOutMap[i] = -2; // unknown
+        p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
+        Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
     }
     return p;
 }