Merged alanmi/abc into default

33 files changed, 2412 insertions, 100 deletions

diff --git a/abclib.dsp b/abclib.dsp
index b852551d..407c3c66 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -271,6 +271,10 @@ SOURCE=.\src\base\abci\abcDsd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcEco.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcExact.c
 # End Source File
 # Begin Source File
@@ -695,6 +699,10 @@ SOURCE=.\src\base\io\ioWriteVerilog.c
 # PROP Default_Filter ""
 # Begin Source File
 
+SOURCE=.\src\base\main\abcapis.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\main\libSupport.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index cc69f6b3..8c0cc161 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -37,7 +37,7 @@ struct Gli_Obj_t_
     unsigned       nFanins  :  3;    // the number of fanins
     unsigned       nFanouts : 25;    // total number of fanouts
     unsigned       Handle;           // ID of the node
-    unsigned       uTruth[2];        // truth table of the node
+    word *         pTruth;           // truth table of the node
     unsigned       uSimInfo;         // simulation info of the node
     union 
     {
@@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
     int i, Phase = 0;
     for ( i = 0; i < (int)pNode->nFanins; i++ )
         Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
-    return Abc_InfoHasBit( pNode->uTruth, Phase );
+    return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase );
 }
 
 /**Function*************************************************************
@@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
     int i, Phase = 0;
     for ( i = 0; i < (int)pNode->nFanins; i++ )
         Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
-    return Abc_InfoHasBit( pNode->uTruth, Phase );
+    return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase );
 }
 
 /**Function*************************************************************
@@ -366,16 +366,15 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth )
+int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth )
 {
     Gli_Obj_t * pObj, * pFanin;
     int i;
-    assert( Vec_IntSize(vFanins) <= 6 );
+    assert( Vec_IntSize(vFanins) <= 16 );
     pObj = Gli_ObjAlloc( p, Vec_IntSize(vFanins), nFanouts );
     Gli_ManForEachEntry( vFanins, p, pFanin, i )
         Gli_ObjAddFanin( pObj, pFanin );
-    pObj->uTruth[0] = puTruth[0];
-    pObj->uTruth[1] = puTruth[Vec_IntSize(vFanins) == 6];
+    pObj->pTruth = pGateTruth;
     pObj->fPhase = pObj->fPhase2 = Gli_NodeComputeValue( pObj );
     return pObj->Handle;
 }
@@ -584,7 +583,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
     int nFanins = Gli_ObjFaninNum(pNode);
     int i, k, Phase;
     Gli_Obj_t * pFanin;
-    assert( nFanins <= 6 );
+    assert( nFanins <= 16 );
     Gli_ObjForEachFanin( pNode, pFanin, i )
         pSimInfos[i] = pFanin->uSimInfo;
     for ( i = 0; i < 32; i++ )
@@ -593,7 +592,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
         for ( k = 0; k < nFanins; k++ )
             if ( (pSimInfos[k] >> i) & 1 )
                 Phase |= (1 << k);
-        if ( Abc_InfoHasBit( pNode->uTruth, Phase ) )
+        if ( Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase ) )
             Result |= (1 << i);
     }
     return Result;
@@ -772,7 +771,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
     }
     if ( fVerbose )
     {
-        printf( "\nSimulated %d patterns.  ", nPatterns );
+        printf( "Simulated %d patterns.  Input transition probability %.2f.  ", nPatterns, PiTransProb );
         ABC_PRMn( "Memory", 4*p->nObjData );
         ABC_PRT( "Time", Abc_Clock() - clk );
     }
diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h
new file mode 100644
index 00000000..d7f425e8
--- /dev/null
+++ b/src/aig/miniaig/ndr.h
@@ -0,0 +1,614 @@
+/**CFile****************************************************************
+
+  FileName    [ndr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Format for word-level design representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: ndr.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__ndr__ndr_h
+#define ABC__base__ndr__ndr_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+//ABC_NAMESPACE_HEADER_START 
+
+#ifdef _WIN32
+#define inline __inline
+#endif
+
+/*
+    For the lack of a better name, this format is called New Data Representation (NDR).
+
+    NDR is based on the following principles:
+    - complex data is composed of individual records
+    - a record has one of several known types (module, name, range, fanins, etc)
+    - a record can be atomic, for example, a name or an operator type
+    - a record can be composed of other records (for example, a module is composed of objects, etc)
+    - the stored data should be easy to write into and read from a file, or pass around as a memory buffer
+    - the format should be simple, easy to use, low-memory, and extensible
+    - new record types can be added by the user as needed
+
+    The implementation is based on the following ideas:
+    - a record is composed of two parts (the header followed by the body)
+    - the header contains two items (the record type and the body size, measured in terms of 4-byte integers)
+    - the body contains as many entries as stated in the record size
+    - if a record is composed of other records, its body contains these records
+
+    As an example, consider a name. It can be a module name, an object name, or a net name.
+    A record storing one name has a header {NDR_NAME, 1} containing record type (NDR_NAME) and size (1),
+    The body of the record is composed of one unsigned integer representing the name (say, 357).  
+    So the complete record looks as follows:  { <header>, <body> } = { {NDR_NAME, 1}, {357} }.
+
+    As another example, consider a two-input AND-gate.  In this case, the recent is composed 
+    of a header {NDR_OBJECT, 4}  containing record type (NDR_OBJECT) and the body size (4), followed 
+    by an array of records creating the AND-gate:  (a) name, (b) operation type, (c) fanins.   
+    The complete record  looks as follows: {  {NDR_OBJECT, 5}, {{{NDR_NAME, 1}, 357}, {{NDR_OPERTYPE, 1}, WLC_OBJ_LOGIC_AND}, 
+    {{NDR_INPUT, 2}, {<id_fanin1>, <id_fanin2>}}} }.   Please note that only body entries are counted towards size. 
+    In the case of one name, there is only one body entry.  In the case of the AND-gate, there are 4 body entries 
+    (name ID, gate type, first fanin, second fanin).
+
+    Headers and bodies of all objects are stored differently.  Headers are stored in an array of unsigned chars, 
+    while bodies are stored in the array of 4-byte unsigned integers.  This is important for memory efficiency. 
+    However, the user does not see these details.
+
+    To estimate memory usage, we can assume that each header takes 1 byte and each body entry contains 4 bytes.   
+    A name takes 5 bytes, and an AND-gate takes 1 * NumHeaders + 4 * NumBodyEntries = 1 * 4 + 4 * 4 = 20 bytes.  
+    Not bad.  The same as memory usage in a well-designed AIG package with structural hashing. 
+
+    Comments:
+    - it is assumed that all port names, net names, and instance names are hashed into 1-based integer numbers called name IDs
+    - nets are not explicitly represented but their name ID are used to establish connectivity between the objects
+    - primary input and primary output objects have to be explicitly created (as shown in the example below)
+    - object inputs are name IDs of the driving nets; object outputs are name IDs of the driven nets
+    - objects can be added to a module in any order
+    - if the ordering of inputs/outputs/flops of a module is not provided as a separate record,
+      their ordering is determined by the order of their appearance of their records in the body of the module
+    - if range limits and signedness are all 0, it is assumed that it is a Boolean object
+    - if left limit and right limit of a range are equal, it is assumed that the range contains one bit
+    - instances of known operators can have types defined by Wlc_ObjType_t below
+    - instances of user modules have type equal to the name ID of the module plus 1000
+    - initial states of the flops are given as char-strings containing 0, 1, and 'x' 
+      (for example, "4'b10XX" is an init state of a 4-bit flop with bit-level init states const1, const0, unknown, unknown)
+    - word-level constants are represented as char-strings given in the same way as they would appear in a Verilog file 
+      (for example, the 16-bit constant 10 is represented as a string "4'b1010". This string contains  8 bytes, 
+      including the char '\0' to denote the end of the string. It will take 2 unsigned ints, therefore 
+      its record will look as follows { {NDR_FUNCTION, 2}, {"4'b1010"} }, but the user does not see these details.  
+      The user only gives  "4'b1010" as an argument (char * pFunction) to the above procedure Ndr_ModuleAddObject(). 
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// record types
+typedef enum {
+    NDR_NONE = 0,          // 0:  unused
+    NDR_DESIGN,            // 1:  design (or library of modules)
+    NDR_MODULE,            // 2:  one module
+    NDR_OBJECT,            // 3:  object
+    NDR_INPUT,             // 4:  input
+    NDR_OUTPUT,            // 5:  output
+    NDR_OPERTYPE,          // 6:  operator type (buffer, shifter, adder, etc)
+    NDR_NAME,              // 7:  name
+    NDR_RANGE,             // 8:  bit range
+    NDR_FUNCTION,          // 9:  specified for some operators (PLAs, etc)
+    NDR_UNKNOWN            // 10: unknown
+} Ndr_RecordType_t; 
+
+// operator types
+typedef enum { 
+    WLC_OBJ_NONE = 0,      // 00: unknown
+    WLC_OBJ_PI,            // 01: primary input 
+    WLC_OBJ_PO,            // 02: primary output
+    WLC_OBJ_FO,            // 03: flop output (unused)
+    WLC_OBJ_FI,            // 04: flop input (unused)
+    WLC_OBJ_FF,            // 05: flop
+    WLC_OBJ_CONST,         // 06: constant
+    WLC_OBJ_BUF,           // 07: buffer
+    WLC_OBJ_MUX,           // 08: multiplexer
+    WLC_OBJ_SHIFT_R,       // 09: shift right
+    WLC_OBJ_SHIFT_RA,      // 10: shift right (arithmetic)
+    WLC_OBJ_SHIFT_L,       // 11: shift left
+    WLC_OBJ_SHIFT_LA,      // 12: shift left (arithmetic)
+    WLC_OBJ_ROTATE_R,      // 13: rotate right
+    WLC_OBJ_ROTATE_L,      // 14: rotate left
+    WLC_OBJ_BIT_NOT,       // 15: bitwise NOT
+    WLC_OBJ_BIT_AND,       // 16: bitwise AND
+    WLC_OBJ_BIT_OR,        // 17: bitwise OR
+    WLC_OBJ_BIT_XOR,       // 18: bitwise XOR
+    WLC_OBJ_BIT_NAND,      // 19: bitwise AND
+    WLC_OBJ_BIT_NOR,       // 20: bitwise OR
+    WLC_OBJ_BIT_NXOR,      // 21: bitwise NXOR
+    WLC_OBJ_BIT_SELECT,    // 22: bit selection
+    WLC_OBJ_BIT_CONCAT,    // 23: bit concatenation
+    WLC_OBJ_BIT_ZEROPAD,   // 24: zero padding
+    WLC_OBJ_BIT_SIGNEXT,   // 25: sign extension
+    WLC_OBJ_LOGIC_NOT,     // 26: logic NOT
+    WLC_OBJ_LOGIC_IMPL,    // 27: logic implication
+    WLC_OBJ_LOGIC_AND,     // 28: logic AND
+    WLC_OBJ_LOGIC_OR,      // 29: logic OR
+    WLC_OBJ_LOGIC_XOR,     // 30: logic XOR
+    WLC_OBJ_COMP_EQU,      // 31: compare equal
+    WLC_OBJ_COMP_NOTEQU,   // 32: compare not equal
+    WLC_OBJ_COMP_LESS,     // 33: compare less
+    WLC_OBJ_COMP_MORE,     // 34: compare more
+    WLC_OBJ_COMP_LESSEQU,  // 35: compare less or equal
+    WLC_OBJ_COMP_MOREEQU,  // 36: compare more or equal
+    WLC_OBJ_REDUCT_AND,    // 37: reduction AND
+    WLC_OBJ_REDUCT_OR,     // 38: reduction OR
+    WLC_OBJ_REDUCT_XOR,    // 39: reduction XOR
+    WLC_OBJ_REDUCT_NAND,   // 40: reduction NAND
+    WLC_OBJ_REDUCT_NOR,    // 41: reduction NOR
+    WLC_OBJ_REDUCT_NXOR,   // 42: reduction NXOR
+    WLC_OBJ_ARI_ADD,       // 43: arithmetic addition
+    WLC_OBJ_ARI_SUB,       // 44: arithmetic subtraction
+    WLC_OBJ_ARI_MULTI,     // 45: arithmetic multiplier
+    WLC_OBJ_ARI_DIVIDE,    // 46: arithmetic division
+    WLC_OBJ_ARI_REM,       // 47: arithmetic remainder
+    WLC_OBJ_ARI_MODULUS,   // 48: arithmetic modulus
+    WLC_OBJ_ARI_POWER,     // 49: arithmetic power
+    WLC_OBJ_ARI_MINUS,     // 50: arithmetic minus
+    WLC_OBJ_ARI_SQRT,      // 51: integer square root
+    WLC_OBJ_ARI_SQUARE,    // 52: integer square
+    WLC_OBJ_TABLE,         // 53: bit table
+    WLC_OBJ_NUMBER         // 54: unused
+} Wlc_ObjType_t;
+
+// printing operator types
+static inline char * Ndr_OperName( int Type )
+{
+    if ( Type == WLC_OBJ_NONE         )   return NULL;
+    if ( Type == WLC_OBJ_PI           )   return "pi";        // 01: primary input 
+    if ( Type == WLC_OBJ_PO           )   return "po";        // 02: primary output (unused)
+    if ( Type == WLC_OBJ_FO           )   return "ff";        // 03: flop output
+    if ( Type == WLC_OBJ_FI           )   return "bi";        // 04: flop input (unused)
+    if ( Type == WLC_OBJ_FF           )   return "ff";        // 05: flop (unused)
+    if ( Type == WLC_OBJ_CONST        )   return "const";     // 06: constant
+    if ( Type == WLC_OBJ_BUF          )   return "buf";       // 07: buffer
+    if ( Type == WLC_OBJ_MUX          )   return "mux";       // 08: multiplexer
+    if ( Type == WLC_OBJ_SHIFT_R      )   return ">>";        // 09: shift right
+    if ( Type == WLC_OBJ_SHIFT_RA     )   return ">>>";       // 10: shift right (arithmetic)
+    if ( Type == WLC_OBJ_SHIFT_L      )   return "<<";        // 11: shift left
+    if ( Type == WLC_OBJ_SHIFT_LA     )   return "<<<";       // 12: shift left (arithmetic)
+    if ( Type == WLC_OBJ_ROTATE_R     )   return "rotR";      // 13: rotate right
+    if ( Type == WLC_OBJ_ROTATE_L     )   return "rotL";      // 14: rotate left
+    if ( Type == WLC_OBJ_BIT_NOT      )   return "~";         // 15: bitwise NOT
+    if ( Type == WLC_OBJ_BIT_AND      )   return "&";         // 16: bitwise AND
+    if ( Type == WLC_OBJ_BIT_OR       )   return "|";         // 17: bitwise OR
+    if ( Type == WLC_OBJ_BIT_XOR      )   return "^";         // 18: bitwise XOR
+    if ( Type == WLC_OBJ_BIT_NAND     )   return "~&";        // 19: bitwise NAND
+    if ( Type == WLC_OBJ_BIT_NOR      )   return "~|";        // 20: bitwise NOR
+    if ( Type == WLC_OBJ_BIT_NXOR     )   return "~^";        // 21: bitwise NXOR
+    if ( Type == WLC_OBJ_BIT_SELECT   )   return "[:]";       // 22: bit selection
+    if ( Type == WLC_OBJ_BIT_CONCAT   )   return "{}";        // 23: bit concatenation
+    if ( Type == WLC_OBJ_BIT_ZEROPAD  )   return "zPad";      // 24: zero padding
+    if ( Type == WLC_OBJ_BIT_SIGNEXT  )   return "sExt";      // 25: sign extension
+    if ( Type == WLC_OBJ_LOGIC_NOT    )   return "!";         // 26: logic NOT
+    if ( Type == WLC_OBJ_LOGIC_IMPL   )   return "=>";        // 27: logic implication
+    if ( Type == WLC_OBJ_LOGIC_AND    )   return "&&";        // 28: logic AND
+    if ( Type == WLC_OBJ_LOGIC_OR     )   return "||";        // 29: logic OR
+    if ( Type == WLC_OBJ_LOGIC_XOR    )   return "^^";        // 30: logic XOR
+    if ( Type == WLC_OBJ_COMP_EQU     )   return "==";        // 31: compare equal
+    if ( Type == WLC_OBJ_COMP_NOTEQU  )   return "!=";        // 32: compare not equal
+    if ( Type == WLC_OBJ_COMP_LESS    )   return "<";         // 33: compare less
+    if ( Type == WLC_OBJ_COMP_MORE    )   return ">";         // 34: compare more
+    if ( Type == WLC_OBJ_COMP_LESSEQU )   return "<=";        // 35: compare less or equal
+    if ( Type == WLC_OBJ_COMP_MOREEQU )   return ">=";        // 36: compare more or equal
+    if ( Type == WLC_OBJ_REDUCT_AND   )   return "&";         // 37: reduction AND
+    if ( Type == WLC_OBJ_REDUCT_OR    )   return "|";         // 38: reduction OR
+    if ( Type == WLC_OBJ_REDUCT_XOR   )   return "^";         // 39: reduction XOR
+    if ( Type == WLC_OBJ_REDUCT_NAND  )   return "~&";        // 40: reduction NAND
+    if ( Type == WLC_OBJ_REDUCT_NOR   )   return "~|";        // 41: reduction NOR
+    if ( Type == WLC_OBJ_REDUCT_NXOR  )   return "~^";        // 42: reduction NXOR
+    if ( Type == WLC_OBJ_ARI_ADD      )   return "+";         // 43: arithmetic addition
+    if ( Type == WLC_OBJ_ARI_SUB      )   return "-";         // 44: arithmetic subtraction
+    if ( Type == WLC_OBJ_ARI_MULTI    )   return "*";         // 45: arithmetic multiplier
+    if ( Type == WLC_OBJ_ARI_DIVIDE   )   return "/";         // 46: arithmetic division
+    if ( Type == WLC_OBJ_ARI_REM      )   return "%";         // 47: arithmetic reminder
+    if ( Type == WLC_OBJ_ARI_MODULUS  )   return "mod";       // 48: arithmetic modulus
+    if ( Type == WLC_OBJ_ARI_POWER    )   return "**";        // 49: arithmetic power
+    if ( Type == WLC_OBJ_ARI_MINUS    )   return "-";         // 50: arithmetic minus
+    if ( Type == WLC_OBJ_ARI_SQRT     )   return "sqrt";      // 51: integer square root
+    if ( Type == WLC_OBJ_ARI_SQUARE   )   return "squar";     // 52: integer square
+    if ( Type == WLC_OBJ_TABLE        )   return "table";     // 53: bit table
+    if ( Type == WLC_OBJ_NUMBER       )   return NULL;        // 54: unused
+    return NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// this is an internal procedure, which is not seen by the user
+typedef struct Ndr_Data_t_  Ndr_Data_t;
+struct Ndr_Data_t_ 
+{
+    int                     nSize;
+    int                     nCap;
+    unsigned char *         pHead;
+    unsigned int *          pBody;
+};
+
+static inline int           Ndr_DataType( Ndr_Data_t * p, int i )                { assert( p->pHead[i] ); return (int)p->pHead[i];                }
+static inline int           Ndr_DataSize( Ndr_Data_t * p, int i )                { return Ndr_DataType(p, i) > NDR_OBJECT ? 1 : p->pBody[i];      }
+static inline int           Ndr_DataEntry( Ndr_Data_t * p, int i )               { return (int)p->pBody[i];                                       }
+static inline int *         Ndr_DataEntryP( Ndr_Data_t * p, int i )              { return (int *)p->pBody + i;                                    }
+static inline int           Ndr_DataEnd( Ndr_Data_t * p, int i )                 { return i + p->pBody[i];                                        }
+static inline void          Ndr_DataAddTo( Ndr_Data_t * p, int i, int Add )      { assert(Ndr_DataType(p, i) <= NDR_OBJECT); p->pBody[i] += Add;  } 
+static inline void          Ndr_DataPush( Ndr_Data_t * p, int Type, int Entry )  { p->pHead[p->nSize] = Type; p->pBody[p->nSize++] = Entry;       }
+
+////////////////////////////////////////////////////////////////////////
+///                          ITERATORS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// iterates over modules in the design
+#define Ndr_DesForEachMod( p, Mod )                                   \
+    for ( Mod = 1; Mod < Ndr_DataEntry(p, 0); Mod += Ndr_DataSize(p, Mod) ) if (Ndr_DataType(p, Mod) != NDR_MODULE) {} else
+
+// iterates over objects in a module
+#define Ndr_ModForEachObj( p, Mod, Obj )                              \
+    for ( Obj = Mod + 1; Obj < Ndr_DataEnd(p, Mod); Obj += Ndr_DataSize(p, Obj) ) if (Ndr_DataType(p, Obj) != NDR_OBJECT) {} else
+
+// iterates over records in an object
+#define Ndr_ObjForEachEntry( p, Obj, Ent )                            \
+    for ( Ent = Obj + 1; Ent < Ndr_DataEnd(p, Obj); Ent += Ndr_DataSize(p, Ent) )
+
+// iterates over primary inputs of a module
+#define Ndr_ModForEachPi( p, Mod, Obj )                               \
+    Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) ) {} else
+
+// iteraots over primary outputs of a module
+#define Ndr_ModForEachPo( p, Mod, Obj )                               \
+    Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else
+
+// iterates over internal nodes of a module
+#define Ndr_ModForEachNode( p, Mod, Obj )                             \
+    Ndr_ModForEachObj( p, 0, Obj ) if ( Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) || Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else
+
+
+////////////////////////////////////////////////////////////////////////
+///                    INTERNAL PROCEDURES                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+static inline void Ndr_DataResize( Ndr_Data_t * p, int Add )
+{
+    if ( p->nSize + Add <= p->nCap )
+        return;
+    p->nCap *= 2;
+    p->pHead = (unsigned char*)realloc( p->pHead,   p->nCap );
+    p->pBody = (unsigned int *)realloc( p->pBody, 4*p->nCap );
+}
+static inline void Ndr_DataPushRange( Ndr_Data_t * p, int RangeLeft, int RangeRight, int fSignedness )
+{ 
+    if ( fSignedness )
+    {
+        Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+        Ndr_DataPush( p, NDR_RANGE, RangeRight );
+        Ndr_DataPush( p, NDR_RANGE, fSignedness );
+        return;
+    }
+    if ( !RangeLeft && !RangeRight )
+        return;
+    if ( RangeLeft == RangeRight )
+        Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+    else
+    {
+        Ndr_DataPush( p, NDR_RANGE, RangeLeft );
+        Ndr_DataPush( p, NDR_RANGE, RangeRight );
+    }
+}
+static inline void Ndr_DataPushArray( Ndr_Data_t * p, int Type, int nArray, int * pArray )
+{ 
+    if ( !nArray )
+        return;
+    assert( nArray > 0 );
+    Ndr_DataResize( p, nArray );
+    memset( p->pHead + p->nSize, Type, nArray );
+    memcpy( p->pBody + p->nSize, pArray, 4*nArray );
+    p->nSize += nArray;
+}
+static inline void Ndr_DataPushString( Ndr_Data_t * p, int Type, char * pFunc )
+{ 
+    if ( !pFunc )
+        return;
+    Ndr_DataPushArray( p, Type, (strlen(pFunc) + 4) / 4, (int *)pFunc );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                     VERILOG WRITING                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Ndr_ObjReadEntry( Ndr_Data_t * p, int Obj, int Type )
+{
+    int Ent;
+    Ndr_ObjForEachEntry( p, Obj, Ent )
+        if ( Ndr_DataType(p, Ent) == Type )
+            return Ndr_DataEntry(p, Ent);
+    return -1;
+}
+static inline int Ndr_ObjReadArray( Ndr_Data_t * p, int Obj, int Type, int ** ppStart )
+{
+    int Ent, Counter = 0; *ppStart = NULL;
+    Ndr_ObjForEachEntry( p, Obj, Ent )
+        if ( Ndr_DataType(p, Ent) == Type )
+        {
+            Counter++;
+            if ( *ppStart == NULL )
+                *ppStart = (int *)p->pBody + Ent;
+        }
+        else if ( *ppStart )
+            return Counter;
+    return Counter;
+} 
+static inline int Ndr_ObjIsType( Ndr_Data_t * p, int Obj, int Type )
+{
+    int Ent;
+    Ndr_ObjForEachEntry( p, Obj, Ent )
+        if ( Ndr_DataType(p, Ent) == NDR_OPERTYPE )
+            return (int)(Ndr_DataEntry(p, Ent) == Type);
+    return -1;
+}
+static inline int Ndr_ObjReadBody( Ndr_Data_t * p, int Obj, int Type )
+{
+    int Ent;
+    Ndr_ObjForEachEntry( p, Obj, Ent )
+        if ( Ndr_DataType(p, Ent) == Type )
+            return Ndr_DataEntry(p, Ent);
+    return -1;
+}
+static inline int * Ndr_ObjReadBodyP( Ndr_Data_t * p, int Obj, int Type )
+{
+    int Ent;
+    Ndr_ObjForEachEntry( p, Obj, Ent )
+        if ( Ndr_DataType(p, Ent) == Type )
+            return Ndr_DataEntryP(p, Ent);
+    return NULL;
+}
+static inline void Ndr_ObjWriteRange( Ndr_Data_t * p, int Obj, FILE * pFile )
+{
+    int * pArray, nArray = Ndr_ObjReadArray( p, Obj, NDR_RANGE, &pArray );
+    if ( nArray == 0 )
+        return;
+    if ( nArray == 3 )
+        fprintf( pFile, "signed " ); 
+    if ( nArray == 1 )
+        fprintf( pFile, "[%d] ", pArray[0] );
+    else
+        fprintf( pFile, "[%d:%d] ", pArray[0], pArray[1] );
+}
+static inline char * Ndr_ObjReadOutName( Ndr_Data_t * p, int Obj, char ** pNames )
+{
+    return pNames[Ndr_ObjReadBody(p, Obj, NDR_OUTPUT)];
+}
+static inline char * Ndr_ObjReadInName( Ndr_Data_t * p, int Obj, char ** pNames )
+{
+    return pNames[Ndr_ObjReadBody(p, Obj, NDR_INPUT)];
+}
+
+// to write signal names, this procedure takes a mapping of name IDs into actual char-strings (pNames)
+static inline void Ndr_ModuleWriteVerilog( char * pFileName, void * pModule, char ** pNames )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pModule; 
+    int Mod = 0, Obj, nArray, * pArray, fFirst = 1;
+
+    FILE * pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
+    if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
+
+    fprintf( pFile, "\nmodule %s (\n  ", pNames[Ndr_ObjReadEntry(p, 0, NDR_NAME)] );
+
+    Ndr_ModForEachPi( p, Mod, Obj )
+        fprintf( pFile, "%s, ", Ndr_ObjReadOutName(p, Obj, pNames) );
+
+    fprintf( pFile, "\n  " );
+
+    Ndr_ModForEachPo( p, Mod, Obj )
+        fprintf( pFile, "%s%s", fFirst ? "":", ", Ndr_ObjReadInName(p, Obj, pNames) ), fFirst = 0;
+
+    fprintf( pFile, "\n);\n\n" );
+
+    Ndr_ModForEachPi( p, Mod, Obj )
+    {
+        fprintf( pFile, "  input " );
+        Ndr_ObjWriteRange( p, Obj, pFile );
+        fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) );
+    }
+
+    Ndr_ModForEachPo( p, Mod, Obj )
+    {
+        fprintf( pFile, "  output " );
+        Ndr_ObjWriteRange( p, Obj, pFile );
+        fprintf( pFile, "%s;\n", Ndr_ObjReadInName(p, Obj, pNames) );
+    }
+
+    Ndr_ModForEachNode( p, Mod, Obj )
+    {
+        fprintf( pFile, "  wire " );
+        Ndr_ObjWriteRange( p, Obj, pFile );
+        fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) );
+    }
+
+    fprintf( pFile, "\n" );
+
+    Ndr_ModForEachNode( p, Mod, Obj )
+    {
+        fprintf( pFile, "  assign %s = ", Ndr_ObjReadOutName(p, Obj, pNames) );
+        nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        if ( nArray == 0 )
+            fprintf( pFile, "%s;\n", (char *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION) );
+        else if ( nArray == 1 && Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_BUF )
+            fprintf( pFile, "%s;\n", pNames[pArray[0]] );
+        else if ( nArray == 1 )
+            fprintf( pFile, "%s %s;\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[0]] );
+        else if ( nArray == 2 )
+            fprintf( pFile, "%s %s %s;\n", pNames[pArray[0]], Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[1]] );
+        else if ( Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_MUX )
+            fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] );
+        else
+            fprintf( pFile, "<cannot write operation %s>;\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) );
+    }
+
+    fprintf( pFile, "\nendmodule\n\n" );
+    fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                     EXTERNAL PROCEDURES                          ///
+////////////////////////////////////////////////////////////////////////
+
+// creating a new module (returns pointer to the memory buffer storing the module info)
+static inline void * Ndr_ModuleCreate( int Name )
+{
+    Ndr_Data_t * p = malloc( sizeof(Ndr_Data_t) );
+    p->nSize = 0;
+    p->nCap  = 16;
+    p->pHead = malloc( p->nCap );
+    p->pBody = malloc( p->nCap * 4 );
+    Ndr_DataPush( p, NDR_MODULE, 0 );
+    Ndr_DataPush( p, NDR_NAME, Name );
+    Ndr_DataAddTo( p, 0, p->nSize );
+    assert( p->nSize == 2 );
+    assert( Name );
+    return p;
+}
+
+// adding a new object (input/output/flop/intenal node) to an already module module
+static inline void Ndr_ModuleAddObject( void * pModule, int Type, int InstName, 
+                                        int RangeLeft, int RangeRight, int fSignedness, 
+                                        int nInputs, int * pInputs, 
+                                        int nOutputs, int * pOutputs, 
+                                        char * pFunction )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pModule;
+    int Obj = p->nSize;  assert( Type != 0 );
+    Ndr_DataResize( p, 6 );
+    Ndr_DataPush( p, NDR_OBJECT, 0 );
+    Ndr_DataPush( p, NDR_OPERTYPE, Type );
+    Ndr_DataPushRange( p, RangeLeft, RangeRight, fSignedness );
+    if ( InstName )
+        Ndr_DataPush( p, NDR_NAME, InstName );
+    Ndr_DataPushArray( p, NDR_INPUT, nInputs, pInputs );
+    Ndr_DataPushArray( p, NDR_OUTPUT, nOutputs, pOutputs );
+    Ndr_DataPushString( p, NDR_FUNCTION, pFunction );
+    Ndr_DataAddTo( p, Obj, p->nSize - Obj );
+    Ndr_DataAddTo( p, 0, p->nSize - Obj );
+    assert( (int)p->pBody[0] == p->nSize );
+}
+
+// deallocate the memory buffer
+static inline void Ndr_ModuleDelete( void * pModule )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pModule;
+    if ( !p ) return;
+    free( p->pHead );
+    free( p->pBody );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                  FILE READING AND WRITING                        ///
+////////////////////////////////////////////////////////////////////////
+
+// file reading/writing
+static inline void * Ndr_ModuleRead( char * pFileName )
+{
+    Ndr_Data_t * p; int nFileSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return NULL; }
+    // check file size
+    fseek( pFile, 0, SEEK_END );
+    nFileSize = ftell( pFile ); 
+    assert( nFileSize % 5 == 0 );
+    rewind( pFile );
+    // create structure
+    p = malloc( sizeof(Ndr_Data_t) );
+    p->nSize = p->nCap = nFileSize / 5;
+    p->pHead = malloc( p->nCap );
+    p->pBody = malloc( p->nCap * 4 );
+    RetValue = fread( p->pBody, 4, p->nCap, pFile );
+    RetValue = fread( p->pHead, 1, p->nCap, pFile );
+    assert( p->nSize == (int)p->pBody[0] );
+    fclose( pFile );
+    return p;
+}
+static inline void Ndr_ModuleWrite( char * pFileName, void * pModule )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pModule; int RetValue;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; }
+    RetValue = fwrite( p->pBody, 4, p->pBody[0], pFile );
+    RetValue = fwrite( p->pHead, 1, p->pBody[0], pFile );
+    fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                     TESTING PROCEDURE                            ///
+////////////////////////////////////////////////////////////////////////
+
+// This testing procedure creates and writes into a Verilog file the following module
+
+// module add10 ( input [3:0] a, output [3:0] s );
+//   wire [3:0] const10 = 4'b1010;
+//   assign s = a + const10;
+// endmodule
+
+static inline void Ndr_ModuleTest()
+{
+    // name IDs
+    int NameIdA = 2;
+    int NameIdS = 3;
+    int NameIdC = 4;
+    // array of fanins of node s
+    int Fanins[2] = { NameIdA, NameIdC };
+    // map name IDs into char strings
+    char * ppNames[5] = { NULL, "add10", "a", "s", "const10" };
+
+    // create a new module
+    void * pModule = Ndr_ModuleCreate( 1 );
+
+    // add objects to the modele
+    Ndr_ModuleAddObject( pModule, WLC_OBJ_PI,       0,   3, 0, 0,   0, NULL,      1, &NameIdA,   NULL      ); // no fanins
+    Ndr_ModuleAddObject( pModule, WLC_OBJ_CONST,    0,   3, 0, 0,   0, NULL,      1, &NameIdC,   "4'b1010" ); // no fanins
+    Ndr_ModuleAddObject( pModule, WLC_OBJ_ARI_ADD,  0,   3, 0, 0,   2, Fanins,    1, &NameIdS,   NULL      ); // fanins are a and const10 
+    Ndr_ModuleAddObject( pModule, WLC_OBJ_PO,       0,   3, 0, 0,   1, &NameIdS,  0, NULL,       NULL      ); // fanin is a
+
+    // write Verilog for verification
+    Ndr_ModuleWriteVerilog( NULL, pModule, ppNames );
+    Ndr_ModuleDelete( pModule );
+}
+
+
+//ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6c0d96d1..fad0b804 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -825,6 +825,7 @@ extern ABC_DLL void               Abc_NtkDontCareFree( Odc_Man_t * p );
 extern ABC_DLL int                Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
 /*=== abcPrint.c ==========================================================*/
 extern ABC_DLL float              Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
+extern ABC_DLL float              Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose );
 extern ABC_DLL void               Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem );
 extern ABC_DLL void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
 extern ABC_DLL void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 466af66a..7fc45f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -61,6 +61,7 @@
 #include "bool/rpo/rpo.h"
 #include "map/mpm/mpm.h"
 #include "opt/fret/fretime.h"
+#include "opt/nwk/nwkMerge.h"
 
 #ifndef _WIN32
 #include <unistd.h>
@@ -121,10 +122,11 @@ static int Abc_CommandMfs                    ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandMfs2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfs3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGlitch                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAddBuffs               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestDec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestNpn                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestRPO                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -315,6 +317,7 @@ static int Abc_CommandPSat                   ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandProve                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEco                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -771,10 +774,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs2",          Abc_CommandMfs2,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs3",          Abc_CommandMfs3,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "glitch",        Abc_CommandGlitch,           0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "addbuffs",      Abc_CommandAddBuffs,         1 );
-//    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
     Cmd_CommandAdd( pAbc, "LogiCS",       "testrpo",       Abc_CommandTestRPO,          0 );
@@ -965,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
+    Cmd_CommandAdd( pAbc, "Verification", "eco",           Abc_CommandEco,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc2",          Abc_CommandBmc2,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc3",          Abc_CommandBmc3,             1 );
@@ -1000,12 +1005,14 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&save",         Abc_CommandAbc9Save,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&load",         Abc_CommandAbc9Load,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&r",            Abc_CommandAbc9Read,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&read",         Abc_CommandAbc9Read,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_blif",    Abc_CommandAbc9ReadBlif,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_cblif",   Abc_CommandAbc9ReadCBlif,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_stg",     Abc_CommandAbc9ReadStg,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_ver",     Abc_CommandAbc9ReadVer,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&write_ver",    Abc_CommandAbc9WriteVer,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&w",            Abc_CommandAbc9Write,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&write",        Abc_CommandAbc9Write,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&wlut",         Abc_CommandAbc9WriteLut,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&ps",           Abc_CommandAbc9Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&pfan",         Abc_CommandAbc9PFan,         0 );
@@ -5715,6 +5722,88 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandGlitch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int nPats    = 4000;
+    int Prob     =    8;
+    int fVerbose =    1;
+    int c;
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NPvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPats = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPats < 1 )
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Prob = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Prob < 1 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsMappedLogic(pNtk) || Abc_NtkGetFaninMax(pNtk) <= 6 )
+        Abc_Print( 1, "Glitching adds %7.2f %% of signal transitions, compared to switching.\n", Abc_NtkMfsTotalGlitching(pNtk, nPats, Prob, fVerbose) );
+    else
+        printf( "Currently computes glitching only for K-LUT networks with K <= 6.\n" );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: glitch [-NP <num>] [-vh]\n" );
+    Abc_Print( -2, "\t           comparing glitching activity to switching activity\n" );
+    Abc_Print( -2, "\t-N <num> : the number of random patterns to use (0 < num < 1000000) [default = %d]\n", nPats );
+    Abc_Print( -2, "\t-P <num> : once in how many cycles an input changes its value [default = %d]\n", Prob );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -6009,7 +6098,7 @@ usage:
     return 1;
 }
 
-#if 0
+//#if 0
 /**Function*************************************************************
 
   Synopsis    []
@@ -6142,7 +6231,7 @@ usage:
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
-#endif
+//#endif
 
 
 
@@ -23862,6 +23951,50 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Abc_NtkEco( char * pFileNames[3] );
+    char * pFileNames[3] = {NULL};  int c;
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( globalUtilOptind + 3 != argc )
+    {
+        Abc_Print( -1, "Expecting three file names on the command line.\n" );
+        return 1;
+    }
+    for ( c = 0; c < 3; c++ )
+        pFileNames[c] = argv[globalUtilOptind+c];
+    Abc_NtkEco( pFileNames );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: eco [-h]\n" );
+    Abc_Print( -2, "\t        performs experimental ECO computation\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -42428,7 +42561,7 @@ usage:
     Abc_Print( -2, "\t-Q num  : stop when abstraction size exceeds num %% during refinement (0<=num<=100) [default = %d]\n", pPars->nRatioMin2 );
     Abc_Print( -2, "\t-P num  : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
     Abc_Print( -2, "\t-B num  : the number of stable frames to call prover or dump abstraction [default = %d]\n", pPars->nFramesNoChangeLim );
-    Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
+    Abc_Print( -2, "\t-A file : file name for dumping abstrated model (&gla -d) or abstraction map (&gla -m)\n" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-r      : toggle using improved refinement heuristics [default = %s]\n", pPars->fNewRefine? "yes": "no" );
diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c
new file mode 100644
index 00000000..70a76729
--- /dev/null
+++ b/src/base/abci/abcEco.c
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+  FileName    [abcEco.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Experimental procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "map/mio/mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkEco( char * pFileNames[3] )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 4e588e2d..f758d0f0 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -923,9 +923,9 @@ void Abc_NtkPrintMiniMapping( int * pArray )
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkOutputMiniMapping( void * pAbc0 )
+int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Vec_Int_t * vMapping;
     int * pArray;
@@ -977,9 +977,9 @@ void Abc_NtkTestMiniMapping( Abc_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
+void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     if ( pAbc == NULL )
@@ -1001,9 +1001,9 @@ void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
     pNode = Abc_NtkCi( pNtk, iCi );
     Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pNode), Rise, Fall );
 }
-void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
+void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     if ( pAbc == NULL )\
@@ -1037,9 +1037,9 @@ void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSetAndGateDelay( void * pAbc0, float Delay )
+void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     if ( pAbc == NULL )
     {
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2129782f..ea91619c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -351,9 +351,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
         Abc_Print( 1,"  power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
     if ( fGlitch )
     {
-        extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
         if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
-            Abc_Print( 1,"  glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+            Abc_Print( 1,"  glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk, 4000, 8, 0) );
         else
             printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." );
     }
@@ -1744,7 +1743,7 @@ extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs );
 extern void        Gli_ManStop( Gli_Man_t * p );
 extern int         Gli_ManCreateCi( Gli_Man_t * p, int nFanouts );
 extern int         Gli_ManCreateCo( Gli_Man_t * p, int iFanin );
-extern int         Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth );
+extern int         Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth );
 
 extern void        Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose );
 extern int         Gli_ObjNumSwitches( Gli_Man_t * p, int iNode );
@@ -1761,13 +1760,14 @@ extern int         Gli_ObjNumGlitches( Gli_Man_t * p, int iNode );
   SeeAlso     []
 
 ***********************************************************************/
-float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
+float Abc_NtkMfsTotalGlitchingLut( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
 {
     int nSwitches, nGlitches;
     Gli_Man_t * p;
     Vec_Ptr_t * vNodes;
     Vec_Int_t * vFanins, * vTruth;
     Abc_Obj_t * pObj, * pFanin;
+    Vec_Wrd_t * vTruths; word * pTruth;
     unsigned * puTruth;
     int i, k;
     assert( Abc_NtkIsLogic(pNtk) );
@@ -1781,6 +1781,7 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
     vNodes = Abc_NtkDfs( pNtk, 0 );
     vFanins = Vec_IntAlloc( 6 );
     vTruth = Vec_IntAlloc( 1 << 12 );
+    vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pNtk) );
 
     // derive network for glitch computation
     p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
@@ -1795,7 +1796,9 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Vec_IntPush( vFanins, pFanin->iTemp );
         puTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 );
-        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth );
+        pTruth = Vec_WrdEntryP( vTruths, Abc_ObjId(pObj) );
+        *pTruth = ((word)puTruth[Abc_ObjFaninNum(pObj) == 6] << 32) | (word)puTruth[0];
+        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), pTruth );
     }
     Abc_NtkForEachCo( pNtk, pObj, i )
         Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
@@ -1816,6 +1819,72 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
     Vec_PtrFree( vNodes );
     Vec_IntFree( vTruth );
     Vec_IntFree( vFanins );
+    Vec_WrdFree( vTruths );
+    return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the percentable of increased power due to glitching.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
+{
+    int nSwitches, nGlitches;
+    Gli_Man_t * p;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vFanins;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFaninMax = Abc_NtkGetFaninMax(pNtk);
+    if ( !Abc_NtkIsMappedLogic(pNtk) )
+        return Abc_NtkMfsTotalGlitchingLut( pNtk, nPats, Prob, fVerbose );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
+    if ( nFaninMax > 16 )
+    {
+        printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" );
+        return -1.0;
+    }
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    vFanins = Vec_IntAlloc( 6 );
+
+    // derive network for glitch computation
+    p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
+        Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->iTemp = -1;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        Vec_IntClear( vFanins );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vFanins, pFanin->iTemp );
+        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), Mio_GateReadTruthP((Mio_Gate_t *)pObj->pData) );
+    }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
+
+    // compute glitching
+    Gli_ManSwitchesAndGlitches( p, nPats, 1.0/Prob, fVerbose );
+
+    // compute the ratio
+    nSwitches = nGlitches = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->iTemp >= 0 )
+        {
+            nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp);
+            nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp);
+        }
+
+    Gli_ManStop( p );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vFanins );
     return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
 }
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b97f526f..abf56716 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDress2.c \
     src/base/abci/abcDress3.c \
     src/base/abci/abcDsd.c \
+    src/base/abci/abcEco.c \
     src/base/abci/abcExact.c \
     src/base/abci/abcExtract.c \
     src/base/abci/abcFraig.c \
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index d1ff0a9d..36e546a7 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_USE_HISTORY 1
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -99,7 +101,7 @@ void Cmd_HistoryAddCommand(    Abc_Frame_t * p, const char * command )
 ***********************************************************************/
 void Cmd_HistoryRead( Abc_Frame_t * p )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
     char Buffer[ABC_MAX_STR];
     FILE * pFile;
     assert( Vec_PtrSize(p->aHistory) == 0 );
@@ -130,7 +132,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
 ***********************************************************************/
 void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
     FILE * pFile;
     char * pStr; 
     int i;
@@ -160,7 +162,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
 ***********************************************************************/
 void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY) 
     char * pStr; 
     int i;
     Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
new file mode 100644
index 00000000..3445a00f
--- /dev/null
+++ b/src/base/main/abcapis.h
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [abcapis.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Include this file in the external code calling ABC.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 29, 2012.]
+
+  Revision    [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef MINI_AIG__abc_apis_h
+#define MINI_AIG__abc_apis_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_Frame_t_      Abc_Frame_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef WIN32
+  #ifdef WIN32_NO_DLL
+    #define ABC_DLLEXPORT
+    #define ABC_DLLIMPORT
+  #else
+    #define ABC_DLLEXPORT __declspec(dllexport)
+    #define ABC_DLLIMPORT __declspec(dllimport)
+  #endif
+#else  /* defined(WIN32) */
+#define ABC_DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL ABC_DLLIMPORT
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern ABC_DLL void   Abc_Start();
+extern ABC_DLL void   Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
+extern ABC_DLL int   Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern ABC_DLL void   Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * pMiniAig );
+extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_NtkSetFlopNum( Abc_Frame_t * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern ABC_DLL void   Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMiniLut );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern ABC_DLL void   Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall );
+extern ABC_DLL void   Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern ABC_DLL void   Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern ABC_DLL int *  Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern ABC_DLL int    Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );   
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );    
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/miniaig/abcapis.h b/src/base/main/abcapis_old.h
index eb8586fe..b2703bea 100644
--- a/src/aig/miniaig/abcapis.h
+++ b/src/base/main/abcapis_old.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef MINI_AIG__abc_apis_h
-#define MINI_AIG__abc_apis_h
+#ifndef MINI_AIG__abc_apis_old_h
+#define MINI_AIG__abc_apis_old_h
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 89353fa6..a59a9a40 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -34,10 +34,8 @@
 #include "misc/vec/vec.h"
 #include "misc/st/st.h"
 
-ABC_NAMESPACE_HEADER_START
-// the framework containing all data
-typedef struct Abc_Frame_t_      Abc_Frame_t;
-ABC_NAMESPACE_HEADER_END
+// the framework containing all data is defined here
+#include "abcapis.h"
 
 #include "base/cmd/cmd.h"
 #include "base/io/ioAbc.h"
@@ -116,7 +114,7 @@ extern ABC_DLL void            Abc_FrameSetBridgeMode();
 
 extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              
-extern ABC_DLL Abc_Cex_t *     Abc_FrameReadCex( Abc_Frame_t * p );              
+extern ABC_DLL void *          Abc_FrameReadCex( Abc_Frame_t * p );              
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexVec( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Int_t *     Abc_FrameReadStatusVec( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadPoEquivs( Abc_Frame_t * p );  
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 9647d020..cd4ff2c7 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -69,7 +69,7 @@ char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagRe
 
 int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
-Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
+void *      Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
 Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p )           { return s_GlobalFrame->vCexVec;      }        
 Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p )        { return s_GlobalFrame->vStatuses;    }        
 Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p )         { return s_GlobalFrame->vPoEquivs;    }        
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 686d9f00..f5dbba42 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -169,9 +169,14 @@ struct Wlc_Par_t_
     int                    nBitsMux;           // MUX bit-width
     int                    nBitsFlop;          // flop bit-width
     int                    nIterMax;           // the max number of iterations
+    int                    nLimit;             // the max number of signals
     int                    fXorOutput;         // XOR outputs of word-level miter
-    int                    fCheckClauses;      // Check clauses in the reloaded trace                    
-    int                    fPushClauses;       // Push clauses in the reloaded trace                    
+    int                    fCheckClauses;      // Check clauses in the reloaded trace
+    int                    fPushClauses;       // Push clauses in the reloaded trace
+    int                    fMFFC;              // Refine the entire MFFC of a PPI
+    int                    fPdra;              // Use pdr -nct
+    int                    fProofRefine;       // Use proof-based refinement
+    int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
@@ -309,6 +314,7 @@ extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 extern char *         Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p );
 extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
 extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
 extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index e33424f7..ad6c6642 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -34,10 +34,616 @@ extern Vec_Vec_t *   IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
 extern int           IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
 extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
 
+typedef struct Int_Pair_t_       Int_Pair_t;
+struct Int_Pair_t_
+{
+    int first;
+    int second;
+};
+
+int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b )
+{
+    return (*a)->second < (*b)->second; 
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) 
+{
+    int num = 0;
+    int i;
+    Wlc_Obj_t * pObj;
+    Wlc_NtkForEachPi(pNtk, pObj, i) {
+        num += Wlc_ObjRange(pObj);
+    }
+    return num;
+}
+
+static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) 
+{
+    Vec_Int_t * vCores = NULL;
+    Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
+    Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames));
+    sat_solver * pSat = sat_solver_new();
+    int i;
+
+    sat_solver_setnvars(pSat, pCnf->nVars);
+
+    for (i = 0; i < pCnf->nClauses; i++) 
+    {
+        if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1]))
+            assert(false);
+    }
+    // add PO clauses
+    {
+        Vec_Int_t* vLits = Vec_IntAlloc(100);
+        Aig_Obj_t* pObj;
+        int i, ret;
+        Aig_ManForEachCo( pAigFrames, pObj, i )
+        {
+            assert(pCnf->pVarNums[pObj->Id] >= 0);
+            Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0));
+        }
+        ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
+        if (!ret) 
+            Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+
+        Vec_IntFree(vLits);
+    }
+    // main procedure
+    {
+        int status;
+        Vec_Int_t* vLits = Vec_IntAlloc(100);
+        Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars );
+        int first_sel_pi = sel_pi_first ? 0 : num_other_pis;
+        for ( i = 0; i < num_sel_pis; ++i ) 
+        {
+            int cur_pi = first_sel_pi + i;
+            int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id];
+            int Lit;
+            assert(var >= 0);
+            Vec_IntWriteEntry( vMapVar2Sel, var, i );
+            Lit = toLitCond( var, 0 );
+            if ( Vec_BitEntry( vMark, i ) )
+                Vec_IntPush(vLits, Lit);
+            else
+                sat_solver_addclause( pSat, &Lit, &Lit+1 );
+        }
+        /*
+            int i, Entry;
+            Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) );
+            Vec_IntForEachEntry(vLits, Entry, i)
+                Abc_Print( 1, "%d ", Entry);
+            Abc_Print( 1, "\n");
+        */
+        status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0));
+        if (status == l_False) {
+            int nCoreLits, *pCoreLits;
+            Abc_Print( 1, "UNSAT.\n" );
+            nCoreLits = sat_solver_final(pSat, &pCoreLits);
+            vCores = Vec_IntAlloc( nCoreLits );
+            for (i = 0; i < nCoreLits; i++) 
+            {
+                Vec_IntPush( vCores, Vec_IntEntry( vMapVar2Sel, lit_var( pCoreLits[i] ) ) );
+            }
+        } else if (status == l_True) {
+            Abc_Print( 1, "SAT.\n" );
+        } else {
+            Abc_Print( 1, "UNKNOWN.\n" );
+        }
+
+        Vec_IntFree(vLits);
+        Vec_IntFree(vMapVar2Sel);
+    }
+    Cnf_ManFree();
+    sat_solver_delete(pSat);
+    Aig_ManStop(pAigFrames);
+
+    return vCores;
+}
+
+static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first) 
+{
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 );
+    int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
+    int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis;
+    int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis;
+    Gia_Man_t * pFrames = NULL;
+    Gia_Obj_t * pObj, * pObjRi;
+    int f, i;
+    int is_sel_pi;
+    Gia_Man_t * pGia;
+    *p_num_ppis = num_ppis;
+
+    Abc_Print( 1, "#orig_pis = %d, #ppis = %d, #sel_pis = %d, #undc_pis = %d\n", nbits_old_pis, num_ppis, num_sel_pis, num_undc_pis );
+    assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis);
+    assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis);
+
+    pFrames = Gia_ManStart( 10000 );
+    pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName );
+    Gia_ManHashAlloc( pFrames );
+    Gia_ManConst0(pGiaChoice)->Value = 0;
+    Gia_ManForEachRi( pGiaChoice, pObj, i )
+        pObj->Value = 0;
+
+    for ( f = 0; f <= pCex->iFrame; f++ ) 
+    {
+        for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ ) 
+        {
+            if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) 
+            {
+                is_sel_pi = sel_pi_first ? (i < nbits_old_pis + num_sel_pis) : (i >= nbits_old_pis + num_ppis);
+                if(f == 0 || !is_sel_pi)
+                    Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+            } 
+            else if (i < nbits_old_pis) 
+            {
+                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
+            } 
+            else if (i >= nbits_old_pis + num_ppis + num_sel_pis) 
+            {
+                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis - num_ppis);
+            }
+        }
+        Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
+            pObj->Value = pObjRi->Value;
+        Gia_ManForEachAnd( pGiaChoice, pObj, i )
+            pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj));
+        Gia_ManForEachCo( pGiaChoice, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        Gia_ManForEachPo( pGiaChoice, pObj, i )
+            Gia_ManAppendCo(pFrames, pObj->Value);
+    }
+    Gia_ManHashStop (pFrames);
+    Gia_ManSetRegNum(pFrames, 0);
+    pFrames = Gia_ManCleanup(pGia = pFrames);
+    Gia_ManStop(pGia);
+    Gia_ManStop(pGiaChoice);
+
+    return pFrames;
+}
+
+Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
+{
+    //if ( vBlacks== NULL ) return NULL;
+    Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    Vec_Int_t * vFanins = Vec_IntAlloc( 3 );
+    Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
+    Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+
+    Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) 
+    {
+        // TODO : fix FOs here
+        Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+    }
+
+    // Vec_IntPrint(vNodes);
+    Wlc_NtkCleanCopy( p );
+
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        pObj->Mark = 1;
+        // add fresh PI with the same number of bits
+        Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
+    }
+
+    // add sel PI
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId( p, pObj );
+        Vec_IntWriteEntry( vMapNode2Sel, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0 ) );
+    }
+
+    // iterate through the nodes in the DFS order
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        int isSigned, range;
+        if ( i == nOrigObjNum ) 
+        {
+            // cout << "break at " << i << endl;
+            break;
+        }
+        if ( pObj->Mark ) 
+        {
+            // clean
+            pObj->Mark = 0;
+
+            isSigned = Wlc_ObjIsSigned(pObj);
+            range = Wlc_ObjRange(pObj);
+            Vec_IntClear(vFanins);
+            Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
+            Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
+            Vec_IntPush(vFanins, i);
+            iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
+        }
+        else 
+        {
+            // update fanins
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        if (iObj != Wlc_ObjCopy(p, iObj)) 
+        {
+            if (pObj->fIsFi)
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
+            else
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
+
+            Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
+        }
+    }
+
+    // DumpWlcNtk(p);
+    pNew = Wlc_NtkDupDfsSimple( p );
+
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vMapNode2Pi );
+    Vec_IntFree( vMapNode2Sel );
+    Vec_IntFree( vNodes );
+    Wlc_NtkFree( p );
+
+    return pNew;
+}
+
+static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops )
+{
+    Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vNodes  = Vec_IntDup( vBlacks );
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
+    Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( !Wlc_ObjIsPi( pObj ) )
+            Vec_IntPush( vFlops, Wlc_ObjId( pNtk, pObj ) ); 
+    }
+
+    Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) 
+        Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        pObj->Mark = 1;
+        // add fresh PI with the same number of bits
+        Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
+    }
+
+    Wlc_NtkCleanCopy( p );
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( i == nOrigObjNum ) 
+            break;
+
+        if ( pObj->Mark ) {
+            // clean
+            pObj->Mark = 0;
+            iObj = Vec_IntEntry( vMapNode2Pi, i );
+        }
+        else {
+            // update fanins
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        if (iObj != Wlc_ObjCopy(p, iObj)) 
+        {
+            if (pObj->fIsFi)
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
+            else
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
+
+
+            Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
+        }
+    }
+
+    pNew = Wlc_NtkDupDfsSimple( p );
+    Vec_IntFree( vMapNode2Pi );
+    Vec_IntFree( vNodes );
+    Wlc_NtkFree( p );
+
+    if ( pvFlops )
+        *pvFlops = vFlops;
+    else
+        Vec_IntFree( vFlops );
+
+    return pNew;
+}
+
+static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
+{
+    Gia_Man_t * pGiaFrames;
+    Vec_Int_t * vRefine = NULL;
+    Vec_Bit_t * vUnmark;
+    Vec_Bit_t * vChoiceMark; 
+    Wlc_Ntk_t * pNtkWithChoices = NULL; 
+    Vec_Int_t * vCoreSels;
+    int num_ppis = -1;
+    int Entry, i;
+
+    if ( *pvRefine == NULL )
+        return 0;
+
+    vUnmark = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+    vChoiceMark = Vec_BitStart( Vec_IntSize( vBlacks ) );      
+
+    Vec_IntForEachEntry( *pvRefine, Entry, i )
+        Vec_BitWriteEntry( vUnmark, Entry, 1 );
+
+    Vec_IntForEachEntry( vBlacks, Entry, i )
+    {
+        if ( Vec_BitEntry( vUnmark, Entry ) )
+            Vec_BitWriteEntry( vChoiceMark, i, 1 );
+    }
+
+    pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
+    pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 );
+    vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars );
+    Wlc_NtkFree( pNtkWithChoices );
+    Gia_ManStop( pGiaFrames );
+    Vec_BitFree( vUnmark );
+    Vec_BitFree( vChoiceMark );
+ 
+    assert( Vec_IntSize( vCoreSels ) );
+
+    vRefine = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vCoreSels, Entry, i )
+        Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) );
+
+    Vec_IntFree( vCoreSels );
+
+    if ( pPars->fVerbose )
+        Abc_Print( 1, "Proof-based refinement reduces %d (out of %d) white boxes\n", Vec_IntSize( *pvRefine ) - Vec_IntSize( vRefine ), Vec_IntSize( *pvRefine ) );
+
+    Vec_IntFree( *pvRefine );
+    *pvRefine = vRefine;
+
+    return 0;
+}
+
+static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark )
+{
+    int Entry, i;
+    Wlc_Obj_t * pObj; int Count[4] = {0};
+    Vec_Int_t * vBlacks = Vec_IntAlloc( 100 );
+
+    assert( *pvBlacks );
+
+    Vec_IntForEachEntry( *pvBlacks, Entry, i )
+    {
+        if ( Vec_BitEntry( vUnmark, Entry) )
+            continue;
+        Vec_IntPush( vBlacks, Entry );
+
+        pObj = Wlc_NtkObj( p, Entry );
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+            Count[0]++;
+        else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+            Count[1]++;
+        else if ( pObj->Type == WLC_OBJ_MUX )
+            Count[2]++;
+        else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+            Count[3]++;
+    }
+    
+    Vec_IntFree( *pvBlacks );
+    *pvBlacks = vBlacks;
+
+    if ( pPars->fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Vec_IntSize( vBlacks ) - Count[0] - Count[1] - Count[2] );
+
+    return 0;
+}
+
+static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Bit_t * vMarks = NULL;
+    Vec_Ptr_t * vAdds  = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vMults = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vFlops = Vec_PtrAlloc( 1000 );
+    Wlc_Obj_t * pObj; int i;
+    Int_Pair_t * pPair;
+
+    if ( pPars->nLimit == ABC_INFINITY )
+        return NULL;
+
+    vMarks = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vAdds, pPair );
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vMults, pPair );
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_MUX ) 
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vMuxes, pPair );
+            }
+        }
+        else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vFlops, pPair );
+            }
+        }
+    }
+
+    Vec_PtrSort( vAdds,  (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vMults, (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vFlops, (int (*)(void))IntPairPtrCompare ) ;
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th ADD has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUL has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break; 
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th FF has width = %d\n", i, pPair->second );
+
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vAdds,  pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrFree( vAdds );
+    Vec_PtrFree( vMults );
+    Vec_PtrFree( vMuxes );
+    Vec_PtrFree( vFlops );
+
+    return vMarks;
+}
+
+static void Wlc_NtkSetUnmark( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark )
+{
+    int Entry, i;
+    Vec_Bit_t * vMarks = Wlc_NtkMarkLimit( p, pPars );
+
+    Vec_BitForEachEntry( vMarks, Entry, i )
+        Vec_BitWriteEntry( vUnmark, i, Entry^1 );
+
+    Vec_BitFree( vMarks );
+}
+
+static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ;
+    Wlc_Obj_t * pObj; int i, Count[4] = {0};
+    Vec_Bit_t * vMarks = NULL;
+
+    vMarks = Wlc_NtkMarkLimit( p, pPars ) ; 
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
+            }
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+            }
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_MUX )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+            }
+            continue;
+        }
+        if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+            }
+            continue;
+        }
+    }
+    if ( vMarks )
+        Vec_BitFree( vMarks );
+    if ( pPars->fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+    return vBlacks;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Mark operators that meet the abstraction criteria.]
@@ -51,6 +657,7 @@ extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu
   SeeAlso     []
 
 ***********************************************************************/
+
 static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
@@ -302,6 +909,17 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
     return nNodes;
 }
 
+static int Wlc_NtkUnmarkRefinement( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+    Wlc_Obj_t * pObj; int i, nNodes = 0;
+    Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+    {
+        Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pObj), 1 );
+        ++nNodes;
+    }
+    return nNodes;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes the map for remapping flop IDs used in the clauses.]
@@ -365,10 +983,12 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF
 int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
     abctime clk = Abc_Clock();
-    abctime pdrClk;
+    abctime clk2;
+    abctime tPdr = 0, tCbr = 0, tPbr = 0, tTotal = 0;
     Pdr_Man_t * pPdr;
     Vec_Vec_t * vClauses = NULL;
     Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL;
+    Vec_Int_t * vBlacks = NULL;
     int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1;
     // start the bitmap to mark objects that cannot be abstracted because of refinement
     // currently, this bitmap is empty because abstraction begins without refinement
@@ -379,12 +999,21 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     pPdrPars->fVerbose   = pPars->fPdrVerbose;
     pPdrPars->fVeryVerbose = 0;
     
+    if ( pPars->fPdra )
+    {
+        pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
+        pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
+        pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
+        pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+    } 
+
     // perform refinement iterations
     for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
     {
         Aig_Man_t * pAig;
         Abc_Cex_t * pCex;
-        Vec_Int_t * vPisNew, * vRefine;  
+        Vec_Int_t * vPisNew = NULL;  
+        Vec_Int_t * vRefine;  
         Gia_Man_t * pGia, * pTemp;
         Wlc_Ntk_t * pAbs;
 
@@ -392,7 +1021,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             printf( "\nIteration %d:\n", nIters );
 
         // get abstracted GIA and the set of pseudo-PIs (vPisNew)
-        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+        if ( pPars->fProofRefine )
+        {
+            if ( vBlacks == NULL )
+                vBlacks = Wlc_NtkGetBlacks( p, pPars );
+            else
+                Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
+            pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew );
+            vPisNew = Vec_IntDup( vBlacks );
+        }
+        else
+        {
+            if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+                Wlc_NtkSetUnmark( p, pPars, vUnmark );
+
+            pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+        }
         pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
 
         // map old flops into new flops
@@ -438,7 +1082,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         pAig = Gia_ManToAigSimple( pGia );
 
         pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
-        pdrClk = Abc_Clock();
+        clk2 = Abc_Clock();
 
         if ( vClauses ) {
             assert( Vec_VecSize( vClauses) >= 2 ); 
@@ -447,7 +1091,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         Vec_IntFreeP( &vMap );
 
         RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
-        pPdr->tTotal += Abc_Clock() - pdrClk;
+        pPdr->tTotal += Abc_Clock() - clk2;
+        tPdr += pPdr->tTotal;
 
         pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
 
@@ -463,7 +1108,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         }
 
         // perform refinement
-        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+        if ( pPars->fHybrid || !pPars->fProofRefine )
+        {
+            clk2 = Abc_Clock();
+            vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+            tCbr += Abc_Clock() - clk2;
+        }
+        else // proof-based only
+        {
+            vRefine = Vec_IntDup( vPisNew );
+        }
+        if ( pPars->fProofRefine ) 
+        {
+            clk2 = Abc_Clock();
+            Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine );
+            tPbr += Abc_Clock() - clk2;
+        }
         Gia_ManStop( pGia );
         Vec_IntFree( vPisNew );
         if ( vRefine == NULL ) // real CEX
@@ -480,14 +1140,29 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         Pdr_ManStop( pPdr );
 
         // update the set of objects to be un-abstracted
-        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
-        if ( pPars->fVerbose )
-            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        clk2 = Abc_Clock();
+        if ( pPars->fMFFC )
+        {
+            nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+            if ( pPars->fVerbose )
+                printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        }
+        else
+        {
+            nNodes = Wlc_NtkUnmarkRefinement( p, vRefine, vUnmark );
+            if ( pPars->fVerbose )
+                printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) );
+
+        }
+        tCbr += Abc_Clock() - clk2;
+
         Vec_IntFree( vRefine );
         Abc_CexFree( pCex );
         Aig_ManStop( pAig );
     }
-
+    
+    if ( vBlacks )
+        Vec_IntFree( vBlacks );
     Vec_IntFreeP( &vFfOld );
     Vec_BitFree( vUnmark );
     // report the result
@@ -501,7 +1176,18 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     else 
         printf( "timed out" );
     printf( " after %d iterations. ", nIters );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    tTotal = Abc_Clock() - clk;
+    Abc_PrintTime( 1, "Time", tTotal );
+
+    if ( pPars->fVerbose )
+    {
+        ABC_PRTP( "PDR          ", tPdr,                          tTotal );
+        ABC_PRTP( "CEX Refine   ", tCbr,                          tTotal );
+        ABC_PRTP( "Proof Refine ", tPbr,                          tTotal );
+        ABC_PRTP( "Misc.        ", tTotal - tPdr - tCbr - tPbr,   tTotal );
+        ABC_PRTP( "Total        ", tTotal,                        tTotal );
+    }
+    
     return RetValue;
 }
 
@@ -550,6 +1236,8 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             printf( "\nIteration %d:\n", nIters );
 
         // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+        if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+            Wlc_NtkSetUnmark( p, pPars, vUnmark );
         pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
         pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index df736e70..38f919d4 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -521,6 +521,26 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIterMax < 0 )
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLimit < 0 )
+                goto usage;
+            break;
+        case 'a':
+            pPars->fPdra ^= 1;
+            break;
+        case 'b':
+            pPars->fProofRefine ^= 1;
+            break;
+        case 'r':
+            pPars->fHybrid ^= 1;
+            break;
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
@@ -530,6 +550,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fPushClauses ^= 1;
             break;
+        case 'm':
+            pPars->fMFFC ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -550,16 +573,21 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
     Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n",               pPars->nLimit );
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle running pdr with -nct [default = %s]\n",                         pPars->fPdra? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle using proof-based refinement [default = %s]\n",                  pPars->fProofRefine? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle using both cex-based and proof-based refinement [default = %s]\n",                  pPars->fHybrid? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",        pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",         pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -585,7 +613,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -644,6 +672,17 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIterMax < 0 )
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLimit < 0 )
+                goto usage;
+            break;
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
@@ -667,13 +706,14 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkAbsCore( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+    Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-xvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
     Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n",               pPars->nLimit );
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index c8fc15a7..89699949 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -108,16 +108,21 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
 void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Wlc_Par_t) );
-    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
-    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-widht 
-    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
-    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
-    pPars->nIterMax    =         1000;   // the max number of iterations
-    pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
-    pPars->fCheckClauses =          1;   // Check clauses in the reloaded trace                    
-    pPars->fPushClauses =           0;   // Push clauses in the reloaded trace                    
-    pPars->fVerbose    =            0;   // verbose output`
-    pPars->fPdrVerbose =            0;   // show verbose PDR output
+    pPars->nBitsAdd      = ABC_INFINITY;   // adder bit-width
+    pPars->nBitsMul      = ABC_INFINITY;   // multiplier bit-widht 
+    pPars->nBitsMux      = ABC_INFINITY;   // MUX bit-width
+    pPars->nBitsFlop     = ABC_INFINITY;   // flop bit-width
+    pPars->nIterMax      =         1000;   // the max number of iterations
+    pPars->nLimit        = ABC_INFINITY;   // the max number of signals
+    pPars->fXorOutput    =            1;   // XOR outputs of word-level miter
+    pPars->fCheckClauses =            1;   // Check clauses in the reloaded trace                    
+    pPars->fPushClauses  =            0;   // Push clauses in the reloaded trace                    
+    pPars->fMFFC         =            1;   // Refine the entire MFFC of a PPI 
+    pPars->fPdra         =            0;   // Use pdr -nct 
+    pPars->fProofRefine  =            0;   // Use proof-based refinement
+    pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
+    pPars->fVerbose      =            0;   // verbose output`
+    pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }
 
 /**Function*************************************************************
@@ -830,6 +835,33 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
         Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
     Wlc_ObjDup( pNew, p, iObj, vFanins );
 }
+
+Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
+{
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    Vec_Int_t * vFanins;
+    int i;
+    Wlc_NtkCleanCopy( p );
+    vFanins = Vec_IntAlloc( 100 );
+    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+    pNew->fSmtLib = p->fSmtLib;
+    Wlc_NtkForEachCi( p, pObj, i )
+        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    if ( p->vInits )
+    pNew->vInits = Vec_IntDup( p->vInits );
+    if ( p->pInits )
+    pNew->pInits = Abc_UtilStrsav( p->pInits );
+    Vec_IntFree( vFanins );
+    if ( p->pSpec )
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    return pNew;
+}
+
 Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
 {
     Wlc_Ntk_t * pNew;
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 49c25ad0..3b747cc5 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
             return 0;
         }
         // report value of this variable
-        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 );
+        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
         Vec_StrFree( vInput );
         fflush( stdout );
     }
diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c
index 9d4653a7..27342458 100644
--- a/src/map/scl/scl.c
+++ b/src/map/scl/scl.c
@@ -1823,13 +1823,17 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     FILE * pFile;
     char * pFileName;
+    int fUseNewFormat = 0;
     int c, fVerbose = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fVerbose ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -1850,25 +1854,29 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-//    Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
 
-    if ( pNtk == NULL )
-    {
-        fprintf( pAbc->Err, "There is no current network.\n" );
-        return 1;
-    }
-
-    // input constraint manager
-    if ( pNtk )
+    if ( !fUseNewFormat )
+        Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
+    else
     {
-        Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
-        if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
+        if ( pNtk == NULL )
+        {
+            fprintf( pAbc->Err, "There is no current network.\n" );
+            return 1;
+        }
+        // input constraint manager
+        if ( pNtk )
+        {
+            Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
+            if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
+        }
     }
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_constr [-vh] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_constr [-nvh] <file>\n" );
     fprintf( pAbc->Err, "\t         read file with timing constraints for standard-cell designs\n" );
+    fprintf( pAbc->Err, "\t-n     : toggle using new constraint file format [default = %s]\n", fUseNewFormat? "yes": "no" );
     fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\t<file> : the name of a file to read\n" );
diff --git a/src/map/scl/sclUtil.c b/src/map/scl/sclUtil.c
index 70140044..07e0deb6 100644
--- a/src/map/scl/sclUtil.c
+++ b/src/map/scl/sclUtil.c
@@ -254,21 +254,21 @@ void Abc_SclReadTimingConstr( Abc_Frame_t * pAbc, char * pFileName, int fVerbose
         pToken = strtok( Buffer, " \t\r\n" );
         if ( pToken == NULL )
             continue;
-//        if ( !strcmp(pToken, "set_driving_cell") )
-        if ( !strcmp(pToken, "default_input_cell") )
+        if ( !strcmp(pToken, "set_driving_cell") )
+//        if ( !strcmp(pToken, "default_input_cell") )
         {
             Abc_FrameSetDrivingCell( Abc_UtilStrsav(strtok(NULL, " \t\r\n")) );
             if ( fVerbose ) 
                 printf( "Setting driving cell to be \"%s\".\n", Abc_FrameReadDrivingCell() );
         }
-//        else if ( !strcmp(pToken, "set_load") )
-        else if ( !strcmp(pToken, "default_output_load") )
+        else if ( !strcmp(pToken, "set_load") )
+//        else if ( !strcmp(pToken, "default_output_load") )
         {
             Abc_FrameSetMaxLoad( atof(strtok(NULL, " \t\r\n")) );
             if ( fVerbose ) 
                 printf( "Setting driving cell to be %f.\n", Abc_FrameReadMaxLoad() );
         }
-//        else printf( "Unrecognized token \"%s\".\n", pToken );
+        else printf( "Unrecognized token \"%s\".\n", pToken );
     }
     fclose( pFile );
 }
diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
index 4d86d2ee..5c5b1f2b 100644
--- a/src/opt/sbd/sbd.c
+++ b/src/opt/sbd/sbd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "misc/vec/vecHsh.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
+{
+    int i, k, Entry = 0, Entry2, Count = 0, Below;
+    int Prev = Vec_IntEntry( vSet, 0 );
+    Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
+    {
+        assert( 2*Prev >= Entry );
+        if ( 2*Prev == Entry )
+        {
+            Prev = Entry;
+            continue;
+        }
+        Below = nVars; 
+        Vec_IntForEachEntryStart( vSet, Entry2, k, i )
+            Below += Entry2;
+        Count += Below * (2*Prev - 1);
+        Prev = Entry;
+    }
+    Count += nVars * 2*Prev;
+    return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
+}
+void Sbd_CountTopos()
+{
+    Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
+    Vec_Int_t * vSet = Vec_IntAlloc( 100 );
+    int i, k, e, Start, Stop;
+    Start = Hsh_VecManAdd( p, vSet );
+    for ( i = 1; i < 9; i++ )
+    {
+        Stop = Hsh_VecSize( p );
+        for ( e = Start; e < Stop; e++ )
+        {
+            Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+            Vec_IntClear( vSet );
+            Vec_IntAppend( vSet, vTemp );
+            for ( k = 0; k < Vec_IntSize(vSet); k++ )
+            {
+                // skip if the number of entries on this level is equal to the number of fanins on the previous level
+                if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
+                    continue;
+                Vec_IntAddToEntry( vSet, k, 1 );
+                Hsh_VecManAdd( p, vSet );
+                Vec_IntAddToEntry( vSet, k, -1 );
+            }
+            Vec_IntPush( vSet, 1 );
+            Hsh_VecManAdd( p, vSet );
+        }
+        printf( "%2d : This = %8d  All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
+        if ( 0 )
+        {
+            for ( e = Stop; e < Hsh_VecSize(p); e++ )
+            {
+                Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+                printf( "Params = %3d.  ", Sbd_CountConfigVars(vTemp, 5) );
+                Vec_IntPrint( vTemp );
+            }
+        }
+        Start = Stop;
+    }
+    Vec_IntFree( vSet );
+    Hsh_VecManStop( p );
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 97a8b644..5f8503a5 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1539,9 +1539,37 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
             pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
         if ( pPars->fDumpVabs || pPars->fDumpMabs )
-            Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
+            Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", 
                 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                 Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
+        if ( pPars->fDumpMabs )
+        {
+            {
+                char Command[1000];
+                Abc_FrameSetStatus( -1 );
+                Abc_FrameSetCex( NULL );
+                Abc_FrameSetNFrames( -1 );
+                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
+                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
+            }
+            {
+                // create trivial abstraction map
+                Gia_Obj_t * pObj; 
+                char * pFileName = Ga2_GlaGetFileName(p, 0);
+                Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
+                pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+                Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+                Gia_ManForEachAnd( pAig, pObj, i )
+                    Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
+                Gia_ManForEachRo( pAig, pObj, i )
+                    Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
+                Gia_AigerWrite( pAig, pFileName, 0, 0 );
+                Vec_IntFree( pAig->vGateClasses );
+                pAig->vGateClasses = vMap;
+                if ( p->pPars->fVerbose )
+                    Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+            }
+        }
         Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
     }
     // iterate unrolling
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 501f9be6..60454752 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -288,7 +288,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
         best_i = i;
         for ( j = i+1; j < nSize; j++ )
 //            if ( pArray[j] < pArray[best_i] )
-            if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
+            if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
                 best_i = j;
         temp = pArray[i];
         pArray[i] = pArray[best_i];
@@ -488,7 +488,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
 
 /**Function*************************************************************
 
-  Synopsis    [Specialized sorting of flops based on cost.]
+  Synopsis    [Specialized sorting of flops based on priority.]
 
   Description []
                
@@ -497,17 +497,171 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
+static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
 {
     int i, j, best_i;
     for ( i = 0; i < nSize-1; i++ )
     {
         best_i = i;
         for ( j = i+1; j < nSize; j++ )
-            if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) )
+            if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
                 best_i = j;
         ABC_SWAP( int, pArray[i], pArray[best_i] );
     }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs generalization using a different idea.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
+{
+    int fUseMinAss = 0;
+    sat_solver * pSat = Pdr_ManFetchSolver( p, k );
+    int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+    Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
+    int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
+    // create free variables
+    int i, iUseVar, iAndVar;
+    iAndVar = Pdr_ManFreeVar(p, k);
+    for ( i = 1; i < nLits; i++ )
+        Pdr_ManFreeVar(p, k);
+    iUseVar = Pdr_ManFreeVar(p, k);
+    for ( i = 1; i < nLits; i++ )
+        Pdr_ManFreeVar(p, k);
+    assert( iUseVar == iAndVar + nLits );
+    // if there is only one positive literal, put it in front and always assume
+    if ( fUseMinAss )
+    {
+        for ( i = 0; i < pCube->nLits && Count < 2; i++ )
+            Count += !Abc_LitIsCompl(pCube->Lits[i]);
+        if ( Count == 1 )
+        {
+            for ( i = 0; i < pCube->nLits; i++ )
+                if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+                    break;
+            assert( i < pCube->nLits );
+            iLit = pCube->Lits[i];
+            for ( ; i > 0; i-- )
+                pCube->Lits[i] = pCube->Lits[i-1];
+            pCube->Lits[0] = iLit;
+        }
+    }
+    // add clauses for the additional AND-gates
+    Vec_IntForEachEntry( vLits1, iLit, i )
+    {
+        sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
+        Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
+    }
+    // add clauses for the additional OR-gate
+    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
+    assert( RetValue == 1 );
+    // add implications
+    vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
+    assert( Vec_IntSize(vLits1) == nLits );
+    Vec_IntForEachEntry( vLits1, iLit, i )
+    {
+        Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
+        Lits[1] = iLit;
+        RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
+        assert( RetValue == 1 );
+        Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
+    }
+    sat_solver_compress( pSat );
+    // perform minimization
+    if ( fUseMinAss )
+    {
+        if ( Count == 1 ) // always assume the only positive literal
+        {
+            if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
+                nLits = 1;
+            else
+                nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
+            sat_solver_pop(pSat); // unassume the first literal
+        }
+        else
+            nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
+        Vec_IntShrink( vLits1, nLits );
+    }
+    else
+    {
+        // try removing one literal at a time in the old-fashioned way
+        int k, Entry;
+        Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
+        for ( i = nLits - 1; i >= 0; i-- )
+        {
+            // if we are about to remove a positive lit, make sure at least one positive lit remains
+            if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
+            {
+                Vec_IntForEachEntry( vLits1, iLit, k )
+                    if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
+                        break;
+                if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
+                    continue;
+            }
+            // load remaining literals
+            Vec_IntClear( vTemp );
+            Vec_IntForEachEntry( vLits1, Entry, k )
+                if ( Entry != -1 && k != i )
+                    Vec_IntPush( vTemp, Entry );
+                else if ( Entry != -1 ) // assume opposite literal
+                    Vec_IntPush( vTemp, Abc_LitNot(Entry) );
+            // solve with assumptions
+            RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
+            // commit the literal
+            if ( RetValue == l_False )
+            {
+                int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
+                int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
+                assert( RetValue );
+            }
+            // update the clause
+            if ( RetValue == l_False )
+                Vec_IntWriteEntry( vLits1, i, -1 );
+        }
+        Vec_IntFree( vTemp );
+        // compact
+        k = 0;
+        Vec_IntForEachEntry( vLits1, Entry, i )
+            if ( Entry != -1 )
+                Vec_IntWriteEntry( vLits1, k++, Entry );
+        Vec_IntShrink( vLits1, k );
+    }
+    // remap auxiliary literals into original literals
+    Vec_IntForEachEntry( vLits1, iLit, i )
+        Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
+    // make sure the cube has at least one positive literal
+    if ( fUseMinAss )
+    {
+        Vec_IntForEachEntry( vLits1, iLit, i )
+            if ( !Abc_LitIsCompl(iLit) )
+                break;
+        if ( i == Vec_IntSize(vLits1) ) // has no positive literals
+        {
+            // find positive lit in the cube
+            for ( i = 0; i < pCube->nLits; i++ )
+                if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+                    break;
+            assert( i < pCube->nLits );
+            Vec_IntPush( vLits1, pCube->Lits[i] );
+//            printf( "-" );
+        }
+//        else
+//            printf( "+" );
+    }
+    // create a subset cube
+    *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
+    assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
+    Order = 0;
+    return 0;
 }
 
 /**Function*************************************************************
@@ -532,7 +686,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     // if there is no induction, return
     *ppCubeMin = NULL;
     if ( p->pPars->fFlopOrder )
-        Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+        Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
     RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
     if ( p->pPars->fFlopOrder )
         Vec_IntSelectSort( pCube->Lits, pCube->nLits );
@@ -543,8 +697,6 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
         p->tGeneral += clock() - clk;
         return 0;
     }
-    
-    keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
 
     // reduce clause using assumptions
 //    pCubeMin = Pdr_SetDup( pCube );
@@ -552,6 +704,31 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     if ( pCubeMin == NULL )
         pCubeMin = Pdr_SetDup( pCube );
 
+    // perform simplified generalization
+    if ( p->pPars->fSimpleGeneral )
+    {
+        assert( pCubeMin->nLits > 0 );
+        if ( pCubeMin->nLits > 1 )
+        {
+            RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
+            Pdr_SetDeref( pCubeMin );
+            assert( ppCubeMin != NULL );
+            pCubeMin = *ppCubeMin;
+        }
+        *ppCubeMin = pCubeMin;
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf("Cube:\n");
+            for ( i = 0; i < pCubeMin->nLits; i++)
+                printf ("%d ", pCubeMin->Lits[i]);
+            printf("\n");
+        }
+        p->tGeneral += Abc_Clock() - clk;
+        return 1;
+    }
+    
+    keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
+
     // perform generalization
     if ( !p->pPars->fSkipGeneral )
     {
@@ -691,9 +868,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     {
         printf("Cube:\n");
         for ( i = 0; i < pCubeMin->nLits; i++)
-        {
-          printf ("%d ", pCubeMin->Lits[i]);
-        }
+            printf ("%d ", pCubeMin->Lits[i]);
         printf("\n");
     }
     *ppCubeMin = pCubeMin;
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 3fcd3d31..8ca8e29e 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -190,6 +190,21 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal )
   SeeAlso     []
 
 ***********************************************************************/
+
+int IPdr_ManRestoreAbsFlops( Pdr_Man_t * p )
+{
+    Pdr_Set_t * pSet; int i, j, k;   
+
+    Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
+    {
+        for ( k = 0; k < pSet->nLits; k++ )
+        {
+            Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
+        }
+    }
+    return 0;
+}
+
 int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap )
 {
     int i;
@@ -288,6 +303,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
                 return 1;
             }
         }
+
+        if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 )
+        {
+            assert( p->vAbsFlops == NULL );
+            p->vAbsFlops  = Vec_IntStart( Saig_ManRegNum(p->pAig) );
+            p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
+            p->vMapPpi2Ff = Vec_IntAlloc( 100 );
+            
+            IPdr_ManRestoreAbsFlops( p );
+        }
+ 
     }
     while ( 1 )
     {
@@ -442,6 +468,9 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
                                 break; // keep solving
                             }
                             p->pAig->pSeqModel = pCex;
+
+                            if ( p->pPars->fVerbose && p->pPars->fUseAbs )
+                                Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
@@ -491,6 +520,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
                 p->timeToStopOne = 0;
             }
         }
+        /*
         if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
         {
             int i, Used;
@@ -498,6 +528,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
                 if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
                     Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
         }
+        */
+        if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
+        {
+            Pdr_Set_t * pSet;
+            int i, j, k;
+            Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 );
+            Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
+                for ( k = 0; k < pSet->nLits; k++ )
+                    Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
+        }
+
         if ( p->pPars->fVerbose )
             Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
         if ( fRefined )
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index cfc608b1..2ac94da5 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -353,11 +353,37 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
+int Bmc_CollapseExpandRound2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit, int fOnOffSetLit )
+{
+    // put into new array
+    int i, iLit, nLits;
+    Vec_IntClear( vTemp );
+    Vec_IntForEachEntry( vLits, iLit, i )
+        if ( iLit != -1 )
+            Vec_IntPush( vTemp, iLit );
+    assert( Vec_IntSize(vTemp) > 0 );
+    // assume condition literal
+    if ( fOnOffSetLit >= 0 )
+        sat_solver_push( pSat, fOnOffSetLit );
+    // minimize
+    nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit );
+    Vec_IntShrink( vTemp, nLits );
+    // assume conditional literal
+    if ( fOnOffSetLit >= 0 )
+        sat_solver_pop( pSat );
+    // modify output literas
+    Vec_IntForEachEntry( vLits, iLit, i )
+        if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 )
+            Vec_IntWriteEntry( vLits, i, -1 );
+    return 0;
+}
+
 int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
 {
     int fProfile = 0;
     int k, n, iLit, status;
     abctime clk;
+    //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit );
     // try removing one literal at a time
     for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- )
     {
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index df9ada8e..fe7e65fe 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2168,6 +2168,153 @@ int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits )
     return status;
 }
 
+// This procedure is called on a set of assumptions to minimize their number.
+// The procedure relies on the fact that the current set of assumptions is UNSAT.  
+// It receives and returns SAT solver without assumptions. It returns the number 
+// of assumptions after minimization. The set of assumptions is returned in pLits.
+int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit )
+{
+    int i, k, nLitsL, nLitsR, nResL, nResR;
+    if ( nLits == 1 )
+    {
+        // since the problem is UNSAT, we will try to solve it without assuming the last literal
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        int status = l_False;
+        int Temp = s->nConfLimit; 
+        s->nConfLimit = nConfLimit;
+        status = sat_solver_solve_internal( s );
+        s->nConfLimit = Temp;
+        return (int)(status != l_False); // return 1 if the problem is not UNSAT
+    }
+    assert( nLits >= 2 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // assume the left lits
+    for ( i = 0; i < nLitsL; i++ )
+        if ( !sat_solver_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver_pop(s);
+            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the right lits
+    nResL = sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
+    for ( i = 0; i < nLitsL; i++ )
+        sat_solver_pop(s);
+    // swap literals
+//    assert( nResL <= nLitsL );
+//    for ( i = 0; i < nResL; i++ )
+//        ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = 0; i < nLitsL; i++ )
+        veci_push( &s->temp_clause, pLits[i] );
+    for ( i = 0; i < nResL; i++ )
+        pLits[i] = pLits[nLitsL+i];
+    for ( i = 0; i < nLitsL; i++ )
+        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+    // assume the right lits
+    for ( i = 0; i < nResL; i++ )
+        if ( !sat_solver_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver_pop(s);
+            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the left lits
+    nResR = sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
+    for ( i = 0; i < nResL; i++ )
+        sat_solver_pop(s);
+    return nResL + nResR;
+}
+
+// This is a specialized version of the above procedure with several custom changes:
+// - makes sure that at least one of the marked literals is preserved in the clause
+// - sets literals to zero when they do not have to be used
+// - sets literals to zero for disproved variables
+int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit )
+{
+    int i, k, nLitsL, nLitsR, nResL, nResR;
+    if ( nLits == 1 )
+    {
+        // since the problem is UNSAT, we will try to solve it without assuming the last literal
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
+        int status = l_False;
+        int Temp = s->nConfLimit; 
+        s->nConfLimit = nConfLimit;
+
+        RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
+        status = sat_solver_solve_internal( s );
+        sat_solver_pop( s );
+
+        // if the problem is UNSAT, add clause
+        if ( status == l_False )
+        {
+            RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+            assert( RetValue );
+        }
+
+        s->nConfLimit = Temp;
+        return (int)(status != l_False); // return 1 if the problem is not UNSAT
+    }
+    assert( nLits >= 2 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // assume the left lits
+    for ( i = 0; i < nLitsL; i++ )
+        if ( !sat_solver_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver_pop(s);
+
+            // add clauses for these literal
+            for ( k = i+1; k > nLitsL; k++ )
+            {
+                int LitNot = Abc_LitNot(pLits[i]);
+                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+                assert( RetValue );
+            }
+
+            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the right lits
+    nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
+    for ( i = 0; i < nLitsL; i++ )
+        sat_solver_pop(s);
+    // swap literals
+//    assert( nResL <= nLitsL );
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = 0; i < nLitsL; i++ )
+        veci_push( &s->temp_clause, pLits[i] );
+    for ( i = 0; i < nResL; i++ )
+        pLits[i] = pLits[nLitsL+i];
+    for ( i = 0; i < nLitsL; i++ )
+        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+    // assume the right lits
+    for ( i = 0; i < nResL; i++ )
+        if ( !sat_solver_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver_pop(s);
+
+            // add clauses for these literal
+            for ( k = i+1; k > nResL; k++ )
+            {
+                int LitNot = Abc_LitNot(pLits[i]);
+                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+                assert( RetValue );
+            }
+
+            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the left lits
+    nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
+    for ( i = 0; i < nResL; i++ )
+        sat_solver_pop(s);
+    return nResL + nResR;
+}
+
+
 
 int sat_solver_nvars(sat_solver* s)
 {
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5a8483c1..5191b2cd 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -50,6 +50,8 @@ extern int         sat_solver_simplify(sat_solver* s);
 extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 extern int         sat_solver_solve_internal(sat_solver* s);
 extern int         sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits);
+extern int         sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit );
+extern int         sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit );
 extern int         sat_solver_push(sat_solver* s, int p);
 extern void        sat_solver_pop(sat_solver* s);
 extern void        sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h
index 2be18cd6..9b05868b 100644
--- a/src/sat/satoko/clause.h
+++ b/src/sat/satoko/clause.h
@@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause)
     printf("}\n");
 }
 
+static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) 
+{
+    unsigned i;
+    for (i = 0; i < clause->size; i++) {
+        int var = (clause->data[i].lit >> 1);
+        char pol = (clause->data[i].lit & 1);
+        fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var));
+    }
+    if (no_zero_var)
+        fprintf(file, "0\n");
+    else
+        fprintf(file, "\n");
+}
+
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__clause_h */
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index adb9a47b..8223affd 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
     vec_uint_free(lits);
     satoko_free(buffer);
     *solver = p;
-    return satoko_simplify(p);
+    return SATOKO_OK;
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index a0c4d216..6634e68e 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -60,6 +60,7 @@ struct satoko_opts {
     unsigned clause_min_lbd_bin_resol;
     float garbage_max_ratio;
     char verbose;
+    char no_simplify;
 };
 
 typedef struct satoko_stats satoko_stats_t;
@@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *);
  */
 extern int satoko_final_conflict(satoko_t *, unsigned *);
 
+/* Procedure to dump a DIMACS file.
+ * - It receives as input the solver, a file name string and two integers.
+ * - If the file name string is NULL the solver will dump in stdout.
+ * - The first argument can be either 0 or 1 and is an option to dump learnt 
+ *   clauses. (value 1 will dump them).
+ * - The seccond argument can be either 0 or 1 and is an option to use 0 as a 
+ *   variable ID or not. Keep in mind that if 0 is used as an ID the generated
+ *   file will not be a DIMACS. (value 1 will use 0 as ID).
+ */
+extern void satoko_write_dimacs(satoko_t *, char *, int, int);
 extern satoko_stats_t satoko_stats(satoko_t *);
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index af3dcffb..42bc6448 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -644,7 +644,7 @@ char solver_search(solver_t *s)
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;
             }
-            if (solver_dlevel(s) == 0)
+            if (!s->opts.no_simplify && solver_dlevel(s) == 0)
                 satoko_simplify(s);
 
             /* Reduce the set of learnt clauses */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 3cb9f3d3..dada33cc 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts)
 {
     memset(opts, 0, sizeof(satoko_opts_t));
     opts->verbose = 0;
+    opts->no_simplify = 0;
     /* Limits */
     opts->conf_limit = 0;
     opts->prop_limit  = 0;
@@ -290,6 +291,10 @@ int satoko_solve(solver_t *s)
     //if (s->opts.verbose)
     //    print_opts(s);
 
+    if (!s->opts.no_simplify)
+        if (satoko_simplify(s) != SATOKO_OK)
+            return SATOKO_UNDEC;
+
     while (status == SATOKO_UNDEC) {
         status = solver_search(s);
         if (solver_check_limits(s) == 0)
@@ -297,6 +302,7 @@ int satoko_solve(solver_t *s)
     }
     if (s->opts.verbose)
         print_stats(s);
+    
     solver_cancel_until(s, vec_uint_size(s->assumptions));
     return status;
 }
@@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
     memcpy(out, vec_uint_data(s->final_conflict),
            sizeof(unsigned) * vec_uint_size(s->final_conflict));
     return vec_uint_size(s->final_conflict);
-
 }
 
 satoko_stats_t satoko_stats(satoko_t *s)
@@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s)
     s->book_cl_lrnt = vec_uint_size(s->learnts);
     s->book_vars = vec_char_size(s->assigns);
     s->book_trail = vec_uint_size(s->trail);
+    s->opts.no_simplify = 1;
 }
 
 void satoko_unbookmark(satoko_t *s)
@@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s)
     s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    s->opts.no_simplify = 0;
 }
 
 void satoko_reset(satoko_t *s)
@@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
         var_clean_mark(s, pvars[i]);
 }
 
+void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
+{
+    FILE *file;
+    unsigned i;
+    unsigned n_vars = vec_act_size(s->activity);
+    unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions);
+    unsigned n_lrnts = vec_uint_size(s->learnts);
+    unsigned *array;
+
+    assert(wrt_lrnt == 0 || wrt_lrnt == 1);
+    assert(zero_var == 0 || zero_var == 1);
+    if (fname != NULL)
+        file = fopen(fname, "w");
+    else
+        file = stdout;
+    
+    if (file == NULL) {
+        printf( "Error: Cannot open output file.\n");
+        return;
+    }
+    fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
+    array = vec_uint_data(s->assumptions);
+    for (i = 0; i < vec_uint_size(s->assumptions); i++)
+        fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var);
+    
+    array = vec_uint_data(s->originals);
+    for (i = 0; i < vec_uint_size(s->originals); i++)
+        clause_dump(file, clause_read(s, array[i]), !zero_var);
+    
+    if (wrt_lrnt) {
+        printf(" Lertns %u", n_lrnts);
+        array = vec_uint_data(s->learnts);
+        for (i = 0; i < n_lrnts; i++)
+            clause_dump(file, clause_read(s, array[i]), !zero_var);
+    }
+
+}
+
+
 ABC_NAMESPACE_IMPL_END