Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

4 files changed, 429 insertions, 86 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 660bf3e1..9d04c0bf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -153,6 +153,7 @@ static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDProve2        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSimSec         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMatch          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -311,6 +312,7 @@ static int Abc_CommandAbc9Force      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Embed      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Era        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Dch        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbcTestNew     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -543,6 +545,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
+    Cmd_CommandAdd( pAbc, "Verification", "dprove2",       Abc_CommandDProve2,          0 );
     Cmd_CommandAdd( pAbc, "Verification", "absec",         Abc_CommandAbSec,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "simsec",        Abc_CommandSimSec,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "match",         Abc_CommandMatch,            0 );
@@ -631,6 +634,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&embed",        Abc_CommandAbc9Embed,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&if",           Abc_CommandAbc9If,           0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&era",          Abc_CommandAbc9Era,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&dch",          Abc_CommandAbc9Dch,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&test",         Abc_CommandAbc9Test,         0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "testnew",         Abc_CommandAbcTestNew,     0 );
@@ -672,6 +676,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
         void For_ManFileExperiment();
 //        For_ManFileExperiment();
     }
+    {
+    }
 
 } 
 
@@ -5437,7 +5443,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Miter computation has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -6539,23 +6545,24 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nIterMax;
     int fPartition;
     int fReorder;
+    int fReorderImage;
     int fVerbose;
     int c;
-    extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
-    extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+    extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nBddMax    = 50000;
-    nIterMax   = 1000;
-    fPartition = 1;
-    fReorder   = 1;
-    fVerbose   = 0;
+    nBddMax       = 50000;
+    nIterMax      = 1000;
+    fPartition    = 1;
+    fReorder      = 1;
+    fReorderImage = 0;
+    fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6587,6 +6594,9 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReorder ^= 1;
             break;
+        case 'o':
+            fReorderImage ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6626,16 +6636,17 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 //    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
-    Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
+    fprintf( pErr, "usage: reach [-BF num] [-provh]\n" );
     fprintf( pErr, "\t         verifies sequential miter using BDD-based reachability\n" );
     fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
     fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
     fprintf( pErr, "\t-p     : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );  
     fprintf( pErr, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );  
+    fprintf( pErr, "\t-o     : toggles BDD variable reordering during image computation [default = %s]\n", fReorderImage? "yes": "no" );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -9554,7 +9565,6 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-
     extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -9564,7 +9574,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9616,6 +9626,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fUseCSat ^= 1;
             break;
+        case 'f':
+            pPars->fLightSynth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -9646,7 +9659,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" );
+    fprintf( pErr, "usage: dch [-WCS num] [-sptgcfvh]\n" );
     fprintf( pErr, "\t         computes structural choices using a new approach\n" );
     fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -9656,6 +9669,7 @@ usage:
     fprintf( pErr, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
     fprintf( pErr, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
     fprintf( pErr, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -16581,7 +16595,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Fra_SecSetDefaultParams( pSecPar );
 //    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijkouwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16686,6 +16700,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'j':
             pSecPar->fInterpolation ^= 1;
             break;
+        case 'k':
+            pSecPar->fInterSeparate ^= 1;
+            break;
+        case 'o':
+            pSecPar->fReorderImage ^= 1;
+            break;
+        case 'u':
+            pSecPar->fReadUnsolved ^= 1;
+            break;
         case 'w':
             pSecPar->fVeryVerbose ^= 1;
             break;
@@ -16712,12 +16735,21 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_NtkDarProve( pNtk, pSecPar );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
 
-    // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
-
+    // read back the resulting unsolved reduced sequential miter
+    if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
+    {
+        char FileName[100];
+        sprintf( FileName, "sm%02d.aig", pSecPar->nSMnumber );
+        pNtk = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
+        if ( pNtk == NULL )
+            printf( "Cannot read back unsolved reduced sequential miter \"%s\",\n", FileName );
+        else
+            Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    }
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" );
+    fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijouwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
     fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
@@ -16734,11 +16766,105 @@ usage:
     fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
     fprintf( pErr, "\t-i     : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" );
     fprintf( pErr, "\t-j     : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" );
-//    fprintf( pErr, "\t-n     : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" );
+    fprintf( pErr, "\t-k     : toggles applying interpolation to each output [default = %s]\n", pSecPar->fInterSeparate? "yes": "no" );
+    fprintf( pErr, "\t-o     : toggles using BDD variable reordering during image computation [default = %s]\n", pSecPar->fReorderImage? "yes": "no" );
+    fprintf( pErr, "\t-u     : toggles reading back unsolved reduced sequential miter [default = %s]\n", pSecPar->fReadUnsolved? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
+} 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDProve2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int nConfLast;
+    int fSeparate;
+    int fVeryVerbose;
+    int fVerbose;
+    int c;
+
+    extern int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nConfLast    = 75000;
+    fSeparate    = 0;
+    fVeryVerbose = 0;
+    fVerbose     = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ckwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLast = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLast < 0 ) 
+                goto usage;
+            break;
+        case 'k':
+            fSeparate ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        printf( "This command works only for sequential networks.\n" );
+        return 0;
+    }
+    // perform verification
+    Abc_NtkDProve2( pNtk, nConfLast, fSeparate, fVeryVerbose, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dprove2 [-C num] [-kwvh]\n" );
+    fprintf( pErr, "\t         improved integrated solver of sequential miters\n" );
+    fprintf( pErr, "\t-C num : the conflict limit during final BMC [default = %d]\n", nConfLast );
+    fprintf( pErr, "\t-k     : toggles solving each output separately [default = %s]\n", fSeparate? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
@@ -18098,7 +18224,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Inter_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbkvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18159,6 +18285,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fUseBackward ^= 1;
             break;
+        case 'k':
+            pPars->fUseSeparate ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -18174,7 +18303,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
-    {
+    { 
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
@@ -18185,10 +18314,29 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
-        fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
-        return 0;
+        if ( pPars->fUseSeparate )
+        {
+            printf( "Each of %d outputs will be solved separately.\n", Abc_NtkPoNum(pNtk) );
+            Abc_NtkDarBmcInter( pNtk, pPars );
+        }
+        else
+        {
+            Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk );
+            printf( "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) );
+            if ( !Abc_NtkCombinePos( pNtkNew, 0 ) )
+            {
+                Abc_NtkDelete( pNtkNew );
+                printf( "ORing outputs has failed.\n" ); 
+                return 0;
+            }
+            Abc_NtkDarBmcInter( pNtkNew, pPars );
+            Abc_NtkDelete( pNtkNew );
+        }
+    }
+    else
+    {
+        Abc_NtkDarBmcInter( pNtk, pPars );
     }
-    Abc_NtkDarBmcInter( pNtk, pPars );
     return 0;
 
 usage:
@@ -18205,6 +18353,7 @@ usage:
     fprintf( pErr, "\t-c     : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
     fprintf( pErr, "\t-g     : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
     fprintf( pErr, "\t-b     : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+    fprintf( pErr, "\t-k     : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -18585,7 +18734,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 usage:
     fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
-    fprintf( pErr, "\t         runs K-step induction for the property output\n" );
+    fprintf( pErr, "\t         runs the inductive case of the K-step induction\n" );
     fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -19959,7 +20108,7 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20005,6 +20154,9 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fSimulateTfo ^= 1;
             break;
+        case 'f':
+            pPars->fLightSynth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -20027,12 +20179,12 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    Aig_ManStop( pAbc->pAbc8Aig );
+//    Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" );
+    fprintf( stdout, "usage: *dch [-WCS num] [-sptfvh]\n" );
     fprintf( stdout, "\t         computes structural choices using a new approach\n" );
     fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -20040,6 +20192,7 @@ usage:
     fprintf( stdout, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
     fprintf( stdout, "\t-p     : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
     fprintf( stdout, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -20973,7 +21126,7 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational.\n" );
         return 0;
     }
 
@@ -21092,7 +21245,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational.\n" );
         return 0;
     }
 
@@ -21285,7 +21438,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "The network is combinational.\n" );
         return 0;
     }
 
@@ -21518,7 +21671,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "The network is combinational.\n" );
         return 0;
     }
 
@@ -23890,7 +24043,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmftcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23936,6 +24089,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fFirstStop ^= 1;
             break;
+        case 't':
+            pPars->fLearnCls ^= 1;
+            break;
         case 'c':
             fCSat ^= 1;
             break;
@@ -23955,7 +24111,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Vec_Int_t * vCounters;
         Vec_Str_t * vStatus;
-        if ( pPars->fNonChrono )
+        if ( pPars->fLearnCls )
+            vCounters = Tas_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+        else if ( pPars->fNonChrono )
             vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
         else
             vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
@@ -23970,7 +24128,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" );
+    fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfctvh]\n" );
     fprintf( stdout, "\t         performs SAT solving for the combinational outputs\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@@ -23979,6 +24137,7 @@ usage:
     fprintf( stdout, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
+    fprintf( stdout, "\t-t     : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -24139,18 +24298,23 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    char * pFileName = "gsrm.aig";
-    Gia_Man_t * pTemp;
+    char * pFileName  = "gsrm.aig";
+    char * pFileName2 = "gsyn.aig";
+    Gia_Man_t * pTemp, * pAux;
     int c, fVerbose = 0;
+    int fSynthesis = 0;
     int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dsvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'd':
             fDualOut ^= 1;
             break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -24165,22 +24329,38 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" );
         return 1;
     } 
-//    pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
-//    Gia_ManStop( pTemp );
     pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
     if ( pTemp )
     {
+        pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
+        Gia_ManStop( pAux );
+
         Gia_WriteAiger( pTemp, pFileName, 0, 0 );
         printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
     }
+    if ( fSynthesis )
+    {
+        pTemp = Gia_ManEquivReduce( pAbc->pAig, 1, fDualOut, fVerbose );
+        if ( pTemp )
+        {
+            pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
+            Gia_ManStop( pAux );
+
+            Gia_WriteAiger( pTemp, pFileName2, 0, 0 );
+            printf( "Reduced original network was written into file \"%s\".\n", pFileName2 );
+            Gia_ManPrintStatsShort( pTemp );
+            Gia_ManStop( pTemp );
+        }
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &srm [-dvh]\n" );
+    fprintf( stdout, "usage: &srm [-dsvh]\n" );
     fprintf( stdout, "\t         writes speculatively reduced model into file \"%s\"\n", pFileName );
     fprintf( stdout, "\t-d     : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
+    fprintf( stdout, "\t-s     : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -24765,7 +24945,7 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int fMiter = 0;
-    int nStatesMax = 1000000;
+    int nStatesMax = 10000000;
     extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
@@ -24834,6 +25014,75 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+//    extern void Hcd_ComputeChoicesTest( Gia_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose );
+    Gia_Man_t * pTemp = NULL;
+    int nBTLimit = 100;
+    int fSynthesis = 1;
+    int fUseMiniSat = 0;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csmvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
+        case 'm':
+            fUseMiniSat ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
+        return 1;
+    } 
+//    Hcd_ComputeChoicesTest( pAbc->pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &dch [-C num] [-smvh]\n" );
+    fprintf( stdout, "\t          computing choices using the latest algorithm\n" );
+    fprintf( stdout, "\t-C num  : the max number of states to traverse (num > 0) [default = %d]\n", nBTLimit );
+    fprintf( stdout, "\t-s      : toggle printing verbose information [default = %s]\n", fSynthesis? "yes": "no" );
+    fprintf( stdout, "\t-m      : toggle using MiniSat as a SAT solver [default = %s]\n", fUseMiniSat? "yes": "no" );
+    fprintf( stdout, "\t-v      : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 873b78d1..1220cb40 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -895,45 +895,37 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
 {
-    extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
-    extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+    extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
+    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 
-    Vec_Ptr_t * vAigs;
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int i, clk;
+    Gia_Man_t * pGia;
+    int clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 clk = clock();
     if ( pPars->fSynthesis )
-    {
-//        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
-        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
-        Aig_ManStop( pMan );
-        // swap around the first and the last
-        pTemp = Vec_PtrPop( vAigs );
-        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
-        Vec_PtrWriteEntry( vAigs, 0, pTemp );
-    }
+        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
     else
     {
-        vAigs = Vec_PtrAlloc( 1 );
-        Vec_PtrPush( vAigs, pMan );
+        pGia = Gia_ManFromAig( pMan );
+        Aig_ManStop( pMan );
     }
 pPars->timeSynth = clock() - clk;
     if ( pPars->fUseGia )
-        pMan = Cec_ComputeChoices( vAigs, pPars );
+        pMan = Cec_ComputeChoices( pGia, pPars );
     else
-        pMan = Dch_ComputeChoices( vAigs, pPars );
+    {
+        pMan = Gia_ManToAigSkip( pGia, 3 );
+        Gia_ManStop( pGia );
+        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+        Aig_ManStop( pTemp );
+    }
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
-//    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
-    // cleanup
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
-        Aig_ManStop( pTemp );
-    Vec_PtrFree( vAigs );
     return pNtkAig;
 }
 
@@ -1535,6 +1527,18 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
     return pNtkAig;
 }
 
+/*
+#include <signal.h>
+#include "utilMem.h"
+static void sigfunc( int signo ) 
+{
+    if (signo == SIGINT) {
+        printf("SIGINT received!\n");
+        s_fInterrupt = 1;
+    }
+}
+*/
+
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -1550,6 +1554,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
+
+/*
+    s_fInterrupt = 0;
+    if ( signal(SIGINT,sigfunc) == SIG_ERR ) 
+    {
+        printf("Could not setup signal handler for SIGINT!\n");
+        return RetValue;
+    }
+    printf("Waiting for SIGINT. Press Ctrl+C to exit.\n");
+//    while ( !s_fInterrupt );
+//    return RetValue;
+*/
+
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -1572,8 +1589,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
             printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
         {
+            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+
             Fra_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+
+            Aig_ManCounterExampleValueTest( pMan, pCex );
         }
     }
     else
@@ -1639,33 +1660,105 @@ ABC_PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
 {
-    Aig_Man_t * pMan;
     int RetValue, iFrame, clk = clock();
-    // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( pMan == NULL )
+    assert( pMan->nRegs > 0 );
+    if ( pPars->fUseSeparate )
     {
-        printf( "Converting miter into AIG has failed.\n" );
-        return -1;
+        Aig_Man_t * pTemp, * pAux;
+        Aig_Obj_t * pObjPo;
+        int i, Counter = 0;
+        Saig_ManForEachPo( pMan, pObjPo, i )
+        {
+            if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
+                continue;
+            pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
+            pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
+            Aig_ManStop( pAux );
+            if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
+            {
+                Aig_ManStop( pTemp );
+                continue;
+            }
+            RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
+            if ( pTemp->pSeqModel )
+            {
+                Ssw_Cex_t * pCex;
+                pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                pCex->iPo = i;
+                Aig_ManStop( pTemp );
+                break;
+            }
+            // if solved, remove the output
+            if ( RetValue == 1 )
+            {
+                Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
+//                    printf( "Output %3d : Solved ", i );
+            }
+            else
+            {
+                Counter++;
+//                    printf( "Output %3d : Undec  ", i );
+            }
+//                Aig_ManPrintStats( pTemp );
+            Aig_ManStop( pTemp );
+            printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
+        }
+        Aig_ManCleanup( pMan );
+        if ( pMan->pSeqModel == NULL )
+        {
+            printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pMan) );
+            if ( Counter )
+                RetValue = -1;
+        }
+/*
+        pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 );
+        Aig_ManStop( pTemp );
+        pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 );
+        Aig_ManStop( pTemp );
+*/
+    }
+    else
+    {    
+        RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     }
-    assert( pMan->nRegs > 0 );
-    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
-    {
         printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-    }
     else if ( RetValue == -1 )
         printf( "Property UNDECIDED.  " );
     else
         assert( 0 );
 ABC_PRT( "Time", clock() - clk );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+{
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    Abc_NtkDarBmcInter_int( pMan, pPars );
+    ABC_FREE( pNtk->pModel );
+    ABC_FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
     return 1;
 }
@@ -2411,7 +2504,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         else
         {
             RetValue = 0;
-            printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
         Gia_ManStop( pGia );
@@ -2439,7 +2532,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         else
         {
             RetValue = 0;
-            printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
         Fra_SmlStop( pSml );
@@ -3187,14 +3280,14 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose )
 {
-    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
+    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
-    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
+    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 36e56e7b..95c7103a 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -157,7 +157,7 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
     if ( pNtk->pManTime == NULL )
         pNtk->pManTime = Abc_ManTimeStart();
     pNtk->pManTime->tReqDef.Rise  = Rise;
-    pNtk->pManTime->tReqDef.Rise  = Fall;
+    pNtk->pManTime->tReqDef.Fall  = Fall;
     pNtk->pManTime->tReqDef.Worst = ABC_MAX( Rise, Fall );
 }
 
@@ -185,7 +185,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     vTimes = pNtk->pManTime->vArrs;
     pTime = vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
-    pTime->Fall  = Rise;
+    pTime->Fall  = Fall;
     pTime->Worst = ABC_MAX( Rise, Fall );
 }
 
@@ -213,7 +213,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     vTimes = pNtk->pManTime->vReqs;
     pTime = vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
-    pTime->Fall  = Rise;
+    pTime->Fall  = Fall;
     pTime->Worst = ABC_MAX( Rise, Fall );
 }
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 9214bb52..aaea7312 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -12,6 +12,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
     src/base/abci/abcDelay.c \
+    src/base/abci/abcDprove2.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcExtract.c \