Adding symbolic fault representation in &fftest.

1 files changed, 208 insertions, 106 deletions

diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index c52b5033..fd33a338 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -53,7 +53,6 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
     memset( p, 0, sizeof(Bmc_ParFf_t) );
     p->pFileName     =  NULL; 
     p->Algo          =     0; 
-    p->fComplVars    =     0; 
     p->fStartPats    =     0; 
     p->nTimeOut      =     0; 
     p->fBasic        =     0; 
@@ -177,7 +176,7 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars )
+Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -202,7 +201,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        iCtrl = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
+        iCtrl = Gia_ManAppendCi(pNew);
         iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( fUseMuxes )
             pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
@@ -228,12 +227,12 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
+Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, iCtrl0, iCtrl1;
-    pNew = Gia_ManStart( (1 + 2 * fUseFaults) * Gia_ManObjNum(p) );
+    int i;
+    pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
@@ -242,13 +241,8 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        if ( fUseFaults )
-        {
-            pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(iCtrl0), pObj->Value );
-            pObj->Value = Gia_ManHashOr( pNew, iCtrl1, pObj->Value );
-        }
+        pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value );
+        pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value );
     }
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
@@ -269,12 +263,12 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
+Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, iCtrl0;
-    pNew = Gia_ManStart( (1 + 3 * fUseFaults) * Gia_ManObjNum(p) );
+    int i;
+    pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
@@ -283,9 +277,7 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        if ( fUseFaults )
-            pObj->Value = Gia_ManHashXor( pNew, iCtrl0, pObj->Value );
+        pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value );
     }
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
@@ -306,12 +298,12 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
+Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB;
-    pNew = Gia_ManStart( (1 + 8 * fUseFaults) * Gia_ManObjNum(p) );
+    pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
@@ -319,26 +311,21 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        iCtrl2 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        iCtrl3 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        if ( fUseFaults )
-        {
-            if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
-                iCtrl0 = Abc_LitNot(iCtrl0);
-            else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
-                iCtrl1 = Abc_LitNot(iCtrl1);
-            else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
-                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 );
-        }
-        else
-            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        iCtrl0 = Gia_ManAppendCi(pNew);
+        iCtrl1 = Gia_ManAppendCi(pNew);
+        iCtrl2 = Gia_ManAppendCi(pNew);
+        iCtrl3 = Gia_ManAppendCi(pNew);
+        if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
+            iCtrl0 = Abc_LitNot(iCtrl0);
+        else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
+            iCtrl1 = Abc_LitNot(iCtrl1);
+        else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
+            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 );
     }
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
@@ -516,7 +503,7 @@ int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr,
 {
     return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars );
 }
-Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm )
+Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm )
 {
     char pStr[100];
     Gia_Man_t * pNew, * pTemp;
@@ -536,15 +523,10 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars,
     Gia_ManForEachAnd( p, pObj, i )
     {
         for ( k = 0; k < nPars; k++ )
-            iCtrl[k] = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
-        if ( fUseFaults )
-        {
-            iFans[0] = Gia_ObjFanin0Copy(pObj);
-            iFans[1] = Gia_ObjFanin1Copy(pObj);
-            pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
-        }
-        else
-            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+            iCtrl[k] = Gia_ManAppendCi(pNew);
+        iFans[0] = Gia_ObjFanin0Copy(pObj);
+        iFans[1] = Gia_ObjFanin1Copy(pObj);
+        pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
     }
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
@@ -701,23 +683,21 @@ void Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Ve
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, int LitRoot, char * pFileName, int fVerbose )
+int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, char * pFileName, int fVerbose )
 {
     FILE * pFile = fopen( pFileName, "wb" );
     Vec_Int_t * vLits;
     Gia_Obj_t * pObj;
     int nItersMax = 10000;
     int i, nIters, status, Value, Count = 0;
-    assert( LitRoot > 1 );
     vLits = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
     for ( nIters = 0; nIters < nItersMax; nIters++ )
     {
-        status = sat_solver_solve( pSat, &LitRoot, &LitRoot+1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_Undef )
-        {
             printf( "Timeout reached after dumping %d untestable faults.\n", nIters );
+        if ( status == l_Undef )
             break;
-        }
         if ( status == l_False )
             break;
         // collect literals
@@ -745,11 +725,12 @@ int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int
             fprintf( pFile, "\n" );
         }
         // add this clause
-        sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
+            break;
     }
     Vec_IntFree( vLits );
     fclose( pFile );
-    return nIters-1;
+    return nIters;
 }
 
 /**Function*************************************************************
@@ -791,6 +772,26 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
 
 /**Function*************************************************************
 
+  Synopsis    [Derive the second AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew )
+{
+    int i;
+    Gia_Man_t * pNew = Gia_ManDup(p);
+    for ( i = 0; i < nPisNew; i++ )
+        Gia_ManAppendCi( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -800,10 +801,10 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
+void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
 {
     int nIterMax = 1000000, nVars, nPars;
-    int i, Iter, LitRoot, status, nFuncVars = -1;
+    int i, Iter, Iter2, status, nFuncVars = -1;
     abctime clkSat = 0, clkTotal = Abc_Clock();
     Vec_Int_t * vLits, * vTests;
     Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
@@ -859,31 +860,21 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
 
     // select algorithm
     if ( pPars->Algo == 0 )
-    {
-        p0 = Gia_ManFormulaUnfold( p, 0, pPars->fComplVars, pPars->pFormStr );
-        p1 = Gia_ManFormulaUnfold( p, 1, pPars->fComplVars, pPars->pFormStr );
-    }
+        p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr );
     else if ( pPars->Algo == 1 )
     {
         assert( Gia_ManRegNum(p) > 0 );
-        p0 = Gia_ManFaultUnfold( p, 0, pPars->fComplVars );
-        p1 = Gia_ManFaultUnfold( p, 1, pPars->fComplVars );
+        p0 = Gia_ManFaultUnfold( pG, 0 );
+        p1 = Gia_ManFaultUnfold( p, 1 );
     }
     else if ( pPars->Algo == 2 )
-    {
-        p0 = Gia_ManStuckAtUnfold( p, 0, pPars->fComplVars );
-        p1 = Gia_ManStuckAtUnfold( p, 1, pPars->fComplVars );
-    }
+        p1 = Gia_ManStuckAtUnfold( p );
     else if ( pPars->Algo == 3 )
-    {
-        p0 = Gia_ManFlipUnfold( p, 0, pPars->fComplVars );
-        p1 = Gia_ManFlipUnfold( p, 1, pPars->fComplVars );
-    }
+        p1 = Gia_ManFlipUnfold( p );
     else if ( pPars->Algo == 4 )
-    {
-        p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars );
-        p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars );
-    }
+        p1 = Gia_ManFOFUnfold( p );
+    if ( pPars->Algo != 1 )
+        p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
 //    Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
 //    printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
 
@@ -895,9 +886,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
 
     // start the SAT solver
     pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars + (pPars->fDumpUntest ? 1 : 0) );
+    sat_solver_setnvars( pSat, pCnf->nVars );
     sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
-    LitRoot = pPars->fDumpUntest ? Abc_Var2Lit( pCnf->nVars, 1 ) : 0;
     // add timeframe clauses
     for ( i = 0; i < pCnf->nClauses; i++ )
         if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
@@ -905,13 +895,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
 
     // add one large OR clause
     vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
-    if ( LitRoot )
-        Vec_IntPush( vLits, Abc_LitNot(LitRoot) );
     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) );
 
-    // add cadinality constraint
+    // add cardinality constraint
     if ( pPars->fBasic )
     {
         Vec_IntClear( vLits );
@@ -930,8 +918,22 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
         for ( Iter = 0; Iter < nTests; Iter++ )
         {
             abctime clk = Abc_Clock();
-            status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+            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 ( pPars->fVerbose )
+                    printf( "\n" );
+                printf( "The problem is UNSAT after adding %d tests.\n", Iter );
+                goto finish;
+            }
             // get pattern
             Vec_IntClear( vLits );
             for ( i = 0; i < nFuncVars; i++ )
@@ -952,20 +954,20 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
     {
         for ( Iter = 0; Iter < 2; Iter++ )
         {
-            status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+            status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_Undef )
             {
                 if ( pPars->fVerbose )
                     printf( "\n" );
-                printf( "Timeout reached after %d seconds and %d iterations.  ", pPars->nTimeOut, Iter );
-                break;
+                printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
+                goto finish;
             }
             if ( status == l_False )
             {
                 if ( pPars->fVerbose )
                     printf( "\n" );
-                printf( "The problem is UNSAT after %d iterations.  ", Iter );
-                break;
+                printf( "The problem is UNSAT after %d iterations.\n", Iter );
+                goto finish;
             }
             // initialize simple pattern
             Vec_IntFill( vLits, nFuncVars, Iter );
@@ -978,7 +980,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
     for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
     {
         abctime clk = Abc_Clock();
-        status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        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 )
         {
@@ -993,8 +995,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
         {
             if ( pPars->fVerbose )
                 printf( "\n" );
-            printf( "Timeout reached after %d seconds and %d iterations.  ", pPars->nTimeOut, Iter );
-            break;
+            printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
+            goto finish;
         }
         if ( status == l_False )
         {
@@ -1017,20 +1019,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
 //    if ( status == l_False )
 //        Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal );
     // cleanup
-    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
-    // dump untestable faults
-    if ( pPars->fDumpUntest )
-    {
-        abctime clk = Abc_Clock();
-        char * pFileName = "untest.txt";
-        int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, Abc_LitNot(LitRoot), pFileName, pPars->fVerbose );
-        printf( "Dumping %d untestable multiple faults into file \"%s\".  ", nUntests, pFileName );
-        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    }
-    Vec_IntFree( vLits );
-    Cnf_DataFree( pCnf );
-    Gia_ManStop( pM );
-    sat_solver_delete( pSat );
+    Abc_PrintTime( 1, "Testing runtime", Abc_Clock() - clkTotal );
     // dump the test suite
     if ( pPars->fDump )
     {
@@ -1038,7 +1027,120 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars )
         Gia_ManDumpTests( vTests, Iter, pFileName );
         printf( "Dumping %d computed test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
     }
+
+    // compute untestable faults
+    if ( p != pG || pPars->fDumpUntest )
+    {
+        abctime clkTotal = Abc_Clock();
+        // restart the SAT solver
+        sat_solver_delete( pSat );
+        pSat = sat_solver_new();
+        sat_solver_setnvars( pSat, pCnf->nVars );
+        sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+        // add timeframe clauses
+        for ( i = 0; i < pCnf->nClauses; i++ )
+            if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+                assert( 0 );
+        // add constraint to rule out no fault
+//        if ( p == pG )
+        {
+            Vec_IntClear( vLits );
+            Gia_ManForEachPi( pM, pObj, i )
+                if ( i >= nFuncVars )
+                    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) );
+        }
+        // add cardinality constraint
+        if ( pPars->fBasic )
+        {
+            Vec_IntClear( vLits );
+            Gia_ManForEachPi( pM, pObj, i )
+                if ( i >= nFuncVars )
+                    Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
+            Cnf_AddCardinConstr( pSat, vLits );
+        }
+        // add output clauses
+        Gia_ManForEachCo( pM, pObj, i )
+        {
+            int Lit = Abc_Var2Lit( pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1 );
+            sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+        }
+        // simplify the SAT solver
+        status = sat_solver_simplify( pSat );
+        assert( status );
+
+        // add test patterns
+        assert( Vec_IntSize(vTests) == Iter * nFuncVars );
+        for ( Iter2 = 0; ; Iter2++ )
+        {
+            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 ( pPars->fVerbose )
+            {
+                printf( "Iter%6d : ",       Iter2 );
+                printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
+                printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+                printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+                //Abc_PrintTime( 1, "Time", clkSat );
+                ABC_PRTr( "Solver time", clkSat );
+            }
+            if ( status == l_Undef )
+            {
+                if ( pPars->fVerbose )
+                    printf( "\n" );
+                printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter2 );
+                goto finish;
+            }
+            if ( Iter2 == Iter )
+                break;
+            assert( status == l_True );
+            // get pattern
+            Vec_IntClear( vLits );
+            for ( i = 0; i < nFuncVars; i++ )
+                Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter2*nFuncVars + i) );
+            Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
+        }
+        assert( Iter2 == Iter );
+        if ( pPars->fVerbose )
+            printf( "\n" );
+        if ( p == pG )
+        {
+            if ( status == l_True )
+                printf( "There are untestable faults.  " );
+            else if ( status == l_False )
+                printf( "There is no untestable faults.  " );
+            else assert( 0 );
+            Abc_PrintTime( 1, "Fault computation runtime", Abc_Clock() - clkTotal );
+        }
+        else
+        {
+            if ( status == l_True )
+                printf( "The circuit is rectifiable.  " );
+            else if ( status == l_False )
+                printf( "The circuit is not rectifiable (or equivalent to the golden one).  " );
+            else assert( 0 );
+            Abc_PrintTime( 1, "Rectification runtime", Abc_Clock() - clkTotal );
+        }
+        // dump untestable faults
+        if ( pPars->fDumpUntest && status == l_True )
+        {
+            abctime clk = Abc_Clock();
+            char * pFileName = "untest.txt";
+            int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
+            if ( p == pG )
+                printf( "Dumped %d untestable multiple faults into file \"%s\".  ", nUntests, pFileName );
+            else
+                printf( "Dumped %d ways of rectifying the circuit into file \"%s\".  ", nUntests, pFileName );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
+    }
+finish:
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pM );
     Vec_IntFree( vTests );
+    Vec_IntFree( vLits );
 }