Making sure reconcile does not change the PO number.

src/aig/bdc/bdcSpfd.c

@@ -811,22 +811,21 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
 void Bdc_SpfdDecomposeTest()
 {
 //    word t = 0x5052585a0002080a;
-
     word t = 0x9ef7a8d9c7193a0f;
 //    word t = 0x6BFDA276C7193A0F;
 //    word t = 0xA3756AFE0B1DF60B;
 
-    int clk = clock();
-//    Vec_Int_t * vWeights;
-//    Vec_Wrd_t * vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
     Vec_Int_t * vWeights;
-    Vec_Wrd_t * vDivs = Bdc_SpfdReadFiles( &vWeights );
-
+    Vec_Wrd_t * vDivs;
     word c0, c1, s, tt, ttt, tbest;
     int i, j, k, n, Cost, CostBest = 100000;
+    int clk = clock();
 
     return;
 
+    // vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
+    vDivs = Bdc_SpfdReadFiles( &vWeights );
+
     Abc_Show6VarFunc( ~t, t );  
 /*
     for ( i = 0; i < 6; i++ )

src/aig/llb/llb4Cex.c

@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose )
+Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose )
 {
     Abc_Cex_t * pCex;
     Cnf_Dat_t * pCnf;
@@ -124,8 +124,18 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int
 
     // add the last frame when the property fails
     Vec_IntClear( vAssumps );
-    Saig_ManForEachPo( pAig, pObj, k )
-        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
+    if ( iCexPo >= 0 )
+    {
+        Saig_ManForEachPo( pAig, pObj, k )
+            if ( k == iCexPo )
+                Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
+    }
+    else
+    {
+        Saig_ManForEachPo( pAig, pObj, k )
+            Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
+    }
+
     // add clause
     status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) );
     if ( status == 0 )
@@ -292,7 +302,7 @@ Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm,
         return NULL;
     }
     // derive updated counter-example
-    pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, 0 );
+    pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, pCexRpm->iPo, 0 );
     Vec_PtrFree( vStates );
     return pCexOrg;
 }

src/aig/llb/llb4Nonlin.c

@@ -742,7 +742,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
             Vec_Ptr_t * vStates;
             assert( p->pAig->pSeqModel == NULL );
             vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose ); 
-            p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, p->pPars->fVerbose );
+            p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose );
             Vec_PtrFreeP( &vStates );
             if ( !p->pPars->fSilent )
             {

src/aig/llb/llbInt.h

@@ -186,7 +186,7 @@ extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager *
 
 
 /*=== llb4Cex.c =======================================================*/
-extern Abc_Cex_t *     Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose );
+extern Abc_Cex_t *     Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose );
 /*=== llb4Cluster.c =======================================================*/
 //extern void            Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
 /*=== llb4Image.c =======================================================*/