Improvements to &fftest (adding computation of fixed parameters).

1 files changed, 206 insertions, 108 deletions

diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 289151b1..5ae44d2f 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -229,11 +229,11 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p )
+Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i;
+    int i, iFuncVars = 0;
     pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -243,9 +243,18 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p )
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value );
-        pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value );
+
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value );
+        else
+            Gia_ManAppendCi(pNew);
+
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value );
+        else
+            Gia_ManAppendCi(pNew);
     }
+    assert( iFuncVars == Vec_IntSize(vMap) );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     pNew = Gia_ManCleanup( pTemp = pNew );
@@ -265,11 +274,11 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p )
+Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i;
+    int i, iFuncVars = 0;
     pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -279,8 +288,12 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p )
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value );
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value );
+        else
+            Gia_ManAppendCi(pNew);
     }
+    assert( iFuncVars == Vec_IntSize(vMap) );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     pNew = Gia_ManCleanup( pTemp = pNew );
@@ -300,11 +313,11 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p )
+Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB;
+    int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
     pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -313,10 +326,26 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        iCtrl0 = Gia_ManAppendCi(pNew);
-        iCtrl1 = Gia_ManAppendCi(pNew);
-        iCtrl2 = Gia_ManAppendCi(pNew);
-        iCtrl3 = Gia_ManAppendCi(pNew);
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            iCtrl0 = Gia_ManAppendCi(pNew);
+        else
+            iCtrl0 = 0, Gia_ManAppendCi(pNew);
+
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            iCtrl1 = Gia_ManAppendCi(pNew);
+        else
+            iCtrl1 = 0, Gia_ManAppendCi(pNew);
+
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            iCtrl2 = Gia_ManAppendCi(pNew);
+        else
+            iCtrl2 = 0, Gia_ManAppendCi(pNew);
+
+        if ( Vec_IntEntry(vMap, iFuncVars++) )
+            iCtrl3 = Gia_ManAppendCi(pNew);
+        else
+            iCtrl3 = 0, Gia_ManAppendCi(pNew);
+
         if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
             iCtrl0 = Abc_LitNot(iCtrl0);
         else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
@@ -325,10 +354,12 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p )
             iCtrl2 = Abc_LitNot(iCtrl2);
         else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
             iCtrl3 = Abc_LitNot(iCtrl3);
+
         iMuxA       = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 );
         iMuxB       = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 );
         pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB,  iMuxA );
     }
+    assert( iFuncVars == Vec_IntSize(vMap) );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     pNew = Gia_ManCleanup( pTemp = pNew );
@@ -803,46 +834,49 @@ Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vLits, int Iter )
+int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vMap, Vec_Int_t * vLits, int Iter )
 {
+    int nConfLimit = 100;
     int status, i, v, iVar, Lit;
     int nUnsats = 0, nRuns = 0;
     abctime clk = Abc_Clock();
-    Vec_IntFill( vLits, Vec_IntSize(vPars), 0 );
+    assert( Vec_IntSize(vPars) == Vec_IntSize(vMap) );
+    // check presence of each variable
+    Vec_IntClear( vLits );
+    Vec_IntAppend( vLits, vMap );
     for ( v = 0; v < Vec_IntSize(vPars); v++ )
     {
-        if ( Vec_IntEntry(vLits, v) )
+        if ( !Vec_IntEntry(vLits, v) )
             continue;
+        assert( Vec_IntEntry(vLits, v) == 1 );
         nRuns++;
         Lit = Abc_Var2Lit( Vec_IntEntry(vPars, v), 0 );
-        status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_Undef )
-        {
-            //printf( "Var %d timed out\n", v );
             continue;
-        }
         if ( status == l_False )
         {
             nUnsats++;
-            //printf( "Var %d is UNSAT\n", v );
+            assert( Vec_IntEntry(vMap, v) == 1 );
+            Vec_IntWriteEntry( vMap, v, 0 );
             Lit = Abc_LitNot(Lit);
             //status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
             //assert( status );
             continue;
         }
         Vec_IntForEachEntry( vPars, iVar, i )
-            if ( !Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) )
-                Vec_IntWriteEntry( vLits, i, 1 );
-        assert( Vec_IntEntry(vLits, v) == 1 );
+            if ( Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) )
+                Vec_IntWriteEntry( vLits, i, 0 );
+        assert( Vec_IntEntry(vLits, v) == 0 );
     }
-    printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls.  ", Iter, nUnsats, Vec_IntSize(vPars), nRuns );
+    printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls.  ", Iter, Vec_IntSize(vMap) - Vec_IntCountPositive(vMap), Vec_IntSize(vPars), nRuns );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return nUnsats;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Generate miter, CNF and solver.]
 
   Description []
                
@@ -851,61 +885,20 @@ int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vLits
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
+int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int nFuncVars, Vec_Int_t * vMap, Vec_Int_t * vTests, Vec_Int_t * vLits, Gia_Man_t ** ppMiter, Cnf_Dat_t ** ppCnf, sat_solver ** ppSat, int fWarmUp )
 {
-    int nIterMax = 1000000, nVars, nPars;
-    int i, Iter, Iter2, status, nFuncVars = -1;
-    abctime clkSat = 0, clkTotal = Abc_Clock();
-    Vec_Int_t * vLits, * vTests, * vPars = NULL;
-    Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
+    Gia_Man_t * p0, * p1, * pM;
     Gia_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
+    int i, Iter, status;
+    abctime clkSat = 0;
 
-    if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) )
-        return;
-
-    // select algorithm
-    if ( pPars->Algo == 0 )
-        printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr );
-    else if ( pPars->Algo == 1 )
-        printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" );
-    else if ( pPars->Algo == 2 )
-        printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" );
-    else if ( pPars->Algo == 3 )
-        printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" );
-    else if ( pPars->Algo == 4 )
-        printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
-    else
-    {
-        printf( "Unrecognized algorithm (%d).\n", pPars->Algo );
-        return;
-    }
-
-    // select algorithm
-    if ( pPars->Algo == 0 )
-        nFuncVars = Gia_ManCiNum(p);
-    else if ( pPars->Algo == 1 )
-        nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
-    else if ( pPars->Algo == 2 )
-        nFuncVars = Gia_ManCiNum(p);
-    else if ( pPars->Algo == 3 )
-        nFuncVars = Gia_ManCiNum(p);
-    else if ( pPars->Algo == 4 )
-        nFuncVars = Gia_ManCiNum(p);
-
-    // collect test patterns from file
-    if ( pPars->pFileName )
-        vTests = Gia_ManGetTestPatterns( pPars->pFileName );
-    else
-        vTests = Vec_IntAlloc( 10000 );
-    if ( vTests == NULL )
-        return;
-    if ( Vec_IntSize(vTests) % nFuncVars != 0 )
+    if ( Vec_IntSize(vTests) && (Vec_IntSize(vTests) % nFuncVars != 0) )
     {
         printf( "The number of symbols in the input patterns (%d) does not divide evenly on the number of test variables (%d).\n", Vec_IntSize(vTests), nFuncVars );
         Vec_IntFree( vTests );
-        return;
+        return 0;
     }
 
     // select algorithm
@@ -918,11 +911,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
         p1 = Gia_ManFaultUnfold( p, 1 );
     }
     else if ( pPars->Algo == 2 )
-        p1 = Gia_ManStuckAtUnfold( p );
+        p1 = Gia_ManStuckAtUnfold( p, vMap );
     else if ( pPars->Algo == 3 )
-        p1 = Gia_ManFlipUnfold( p );
+        p1 = Gia_ManFlipUnfold( p, vMap );
     else if ( pPars->Algo == 4 )
-        p1 = Gia_ManFOFUnfold( p );
+        p1 = Gia_ManFOFUnfold( p, vMap );
     if ( pPars->Algo != 1 )
         p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
 //    Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
@@ -944,7 +937,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
             assert( 0 );
 
     // add one large OR clause
-    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+    Vec_IntClear( vLits );
     Gia_ManForEachCo( pM, pObj, i )
         Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
     sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
@@ -964,25 +957,31 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
     {
         int nTests = Vec_IntSize(vTests) / nFuncVars;
         assert( Vec_IntSize(vTests) % nFuncVars == 0 );
-        printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName );
+        if ( pPars->pFileName )
+            printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName );
+        else
+            printf( "Reading %d pre-computed test patterns from previous rounds.\n", Vec_IntSize(vTests) / nFuncVars );
         for ( Iter = 0; Iter < nTests; Iter++ )
         {
-            abctime clk = Abc_Clock();
-            status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-            clkSat += Abc_Clock() - clk;
-            if ( status == l_Undef )
-            {
-                if ( pPars->fVerbose )
-                    printf( "\n" );
-                printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter );
-                goto finish;
-            }
-            if ( status == l_False )
+            if ( fWarmUp )
             {
-                if ( pPars->fVerbose )
-                    printf( "\n" );
-                printf( "The problem is UNSAT after adding %d tests.\n", Iter );
-                goto finish;
+                abctime clk = Abc_Clock();
+                status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+                clkSat += Abc_Clock() - clk;
+                if ( status == l_Undef )
+                {
+                    if ( pPars->fVerbose )
+                        printf( "\n" );
+                    printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter );
+                    return 0;
+                }
+                if ( status == l_False )
+                {
+                    if ( pPars->fVerbose )
+                        printf( "\n" );
+                    printf( "The problem is UNSAT after adding %d tests.\n", Iter );
+                    return 0;
+                }
             }
             // get pattern
             Vec_IntClear( vLits );
@@ -1010,14 +1009,14 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
                 if ( pPars->fVerbose )
                     printf( "\n" );
                 printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
-                goto finish;
+                return 0;
             }
             if ( status == l_False )
             {
                 if ( pPars->fVerbose )
                     printf( "\n" );
                 printf( "The problem is UNSAT after %d iterations.\n", Iter );
-                goto finish;
+                return 0;
             }
             // initialize simple pattern
             Vec_IntFill( vLits, nFuncVars, Iter );
@@ -1026,10 +1025,120 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
         }
     }
 
+    printf( "Using miter with:  AIG nodes = %6d.  CNF variables = %6d.  CNF clauses = %8d.\n", Gia_ManAndNum(pM), pCnf->nVars, pCnf->nClauses );
+
+    *ppMiter = pM;
+    *ppCnf = pCnf;
+    *ppSat = pSat;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
+{
+    int nIterMax = 1000000, nVars, nPars;
+    int i, Iter, Iter2, status, nFuncVars = -1;
+    abctime clk, clkSat = 0, clkTotal = Abc_Clock();
+    Vec_Int_t * vLits, * vMap = NULL, * vTests, * vPars = NULL;
+    Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
+    Gia_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+
+    if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) )
+        return;
+
+    // select algorithm
+    if ( pPars->Algo == 0 )
+        printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr );
+    else if ( pPars->Algo == 1 )
+        printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 2 )
+        printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 3 )
+        printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" );
+    else if ( pPars->Algo == 4 )
+        printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
+    else
+    {
+        printf( "Unrecognized algorithm (%d).\n", pPars->Algo );
+        return;
+    }
+
+    // select algorithm
+    if ( pPars->Algo == 0 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( pPars->Algo == 1 )
+        nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
+    else if ( pPars->Algo == 2 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( pPars->Algo == 3 )
+        nFuncVars = Gia_ManCiNum(p);
+    else if ( pPars->Algo == 4 )
+        nFuncVars = Gia_ManCiNum(p);
+
+    // collect test patterns from file
+    if ( pPars->pFileName )
+        vTests = Gia_ManGetTestPatterns( pPars->pFileName );
+    else
+        vTests = Vec_IntAlloc( 10000 );
+    if ( vTests == NULL )
+        return;
+
+    // select algorithm
+    vMap = Vec_IntAlloc( 0 );
+    if ( pPars->Algo == 2 )
+        Vec_IntFill( vMap, 2 * Gia_ManAndNum(p), 1 );
+    else if ( pPars->Algo == 3 )
+        Vec_IntFill( vMap,     Gia_ManAndNum(p), 1 );
+    else if ( pPars->Algo == 4 )
+        Vec_IntFill( vMap, 4 * Gia_ManAndNum(p), 1 );
+
+    // prepare SAT solver
+    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+    if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 1) )
+        return;
+
     // iterate through the test vectors
     for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
     {
-        abctime clk = Abc_Clock();
+        // collect parameter variables
+        if ( pPars->nIterCheck && vPars == NULL )
+        {
+            vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
+            Gia_ManForEachPi( pM, pObj, i )
+                if ( i >= nFuncVars )
+                    Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
+            assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars );
+        }
+        // derive unit parameter variables
+        if ( Iter && pPars->nIterCheck && (Iter % pPars->nIterCheck) == 0 )
+        {
+            Gia_ManFaultAnalyze( pSat, vPars, vMap, vLits, Iter );
+            // cleanup
+            Gia_ManStop( pM );
+            Cnf_DataFree( pCnf );
+            sat_solver_delete( pSat );
+            // recompute
+            if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 0) )
+            {
+                printf( "This should never happen.\n" );
+                return;
+            }
+            Vec_IntFreeP( &vPars );
+        }
+        // solve
+        clk = Abc_Clock();
         status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         clkSat += Abc_Clock() - clk;
         if ( pPars->fVerbose )
@@ -1064,18 +1173,6 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
         Vec_IntAppend( vTests, vLits );
         // add constraint
         Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
-        // collect parameter variables
-        if ( pPars->nIterCheck && vPars == NULL )
-        {
-            vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
-            Gia_ManForEachPi( pM, pObj, i )
-                if ( i >= nFuncVars )
-                    Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
-            assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars );
-        }
-        // derive unit parameter variables
-        if ( pPars->nIterCheck && !(Iter % pPars->nIterCheck) )
-            Gia_ManFaultAnalyze( pSat, vPars, vLits, Iter );
     }
 finish:
     // print results
@@ -1202,6 +1299,7 @@ finish:
     Cnf_DataFree( pCnf );
     Gia_ManStop( pM );
     Vec_IntFree( vTests );
+    Vec_IntFree( vMap );
     Vec_IntFree( vLits );
     Vec_IntFreeP( &vPars );
 }