5 files changed, 36 insertions, 12 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 3c40d2d5..a815bb30 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -71,7 +71,7 @@ struct Pdr_Par_t_
 
 /*=== pdrCore.c ==========================================================*/
 extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index f72983da..76d6f788 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -635,7 +635,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 
                         if ( !p->pPars->fSolveAll )
                         {
-                            p->pAig->pSeqModel = Pdr_ManDeriveCex( p );
+                            p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
@@ -647,6 +647,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
+                        Pdr_QueueClean( p );
+                        pCube = NULL;
+                        break; // keep solving
                     }
                     if ( p->pPars->fVerbose ) 
                         Pdr_ManPrintProgress( p, 0, clock() - clkStart );
@@ -735,7 +738,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
 {
     Pdr_Man_t * p;
     int RetValue;
@@ -743,16 +746,19 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     if ( pPars->fVerbose )
     {
 //    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
-        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", 
-            pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
-        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", 
-            pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ", 
+            pPars->nRecycle, 
+            pPars->nFrameMax, 
+            pPars->nRestLimit, 
+            pPars->nTimeOut );
+        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n", 
+            pPars->fMonoCnf ?     "yes" : "no", 
+            pPars->fSkipGeneral ? "yes" : "no", 
+            pPars->fSolveAll ?    "yes" : "no" );
     }
     ABC_FREE( pAig->pSeqModel );
     p = Pdr_ManStart( pAig, pPars, NULL );
     RetValue = Pdr_ManSolveInt( p );
-//    if ( ppCex )
-//        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
     if ( RetValue == 0 )
         assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
     if ( p->vCexes )
@@ -763,9 +769,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     }
     if ( p->pPars->fDumpInv )
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-//    if ( *ppCex && pPars->fVerbose )
-//        Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n", 
-//            (*ppCex)->iFrame, p->nFrames );
     p->tTotal += clock() - clk;
     Pdr_ManStop( p );
     pPars->iFrame--;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index abc8f12b..f6d3d170 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -187,6 +187,7 @@ extern void            Pdr_OblDeref( Pdr_Obl_t * p );
 extern int             Pdr_QueueIsEmpty( Pdr_Man_t * p );
 extern Pdr_Obl_t *     Pdr_QueueHead( Pdr_Man_t * p );
 extern Pdr_Obl_t *     Pdr_QueuePop( Pdr_Man_t * p );
+extern void            Pdr_QueueClean( Pdr_Man_t * p );
 extern void            Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
 extern void            Pdr_QueuePrint( Pdr_Man_t * p );
 extern void            Pdr_QueueStop( Pdr_Man_t * p );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 78aa2b69..95e7641b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -188,6 +188,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
         }
     assert( f == nFrames );
+    if ( !Saig_ManVerifyCex(p->pAig, pCex) )
+        printf( "CEX for output %d is not valid.\n", p->iOutCur );
     return pCex;
 }
 
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index a47bc9f0..c70554e3 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -510,6 +510,24 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Pdr_QueueClean( Pdr_Man_t * p )
+{
+    Pdr_Obl_t * pThis;
+    while ( (pThis = Pdr_QueuePop(p)) )
+        Pdr_OblDeref( pThis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
 {
     Pdr_Obl_t * pTemp, ** ppPrev;