Version abc80205

author: Alan Mishchenko <alanmi@berkeley.edu> 2008-02-05 08:01:00 -0800
committer: Alan Mishchenko <alanmi@berkeley.edu> 2008-02-05 08:01:00 -0800
commit: 7174787abafe80437892b55a53f994da85a37342 (patch)
tree: 0df4c6f35d99111d757aa9b8091853b8f88ee762
parent: 3b790eb17e54cd922440a1a3b18a5cfdd5cbcadb (diff)
download: abc-7174787abafe80437892b55a53f994da85a37342.tar.gz
abc-7174787abafe80437892b55a53f994da85a37342.tar.bz2
abc-7174787abafe80437892b55a53f994da85a37342.zip
29 files changed, 4800 insertions, 91 deletions
diff --git a/abc.dsp b/abc.dsp
index 03abc5ea..5830eeb8 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1626,14 +1626,26 @@ SOURCE=.\src\opt\mfs\mfsCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\mfs\mfsDiv.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\mfs\mfsInt.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\mfs\mfsInter.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\mfs\mfsMan.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\mfs\mfsResub.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\mfs\mfsSat.c
 # End Source File
 # Begin Source File
diff --git a/abc.plg b/abc.plg
new file mode 100644
index 00000000..8c7808b2
--- /dev/null
+++ b/abc.plg
@@ -0,0 +1,1201 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abc - Win32 Release--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB41.tmp" with contents
+[
+/nologo /ML /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
+"C:\_projects\abc\src\opt\mfs\mfsMan.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB41.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB42.tmp" with contents
+[
+kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe" 
+.\Release\abcAig.obj
+.\Release\abcBlifMv.obj
+.\Release\abcCheck.obj
+.\Release\abcDfs.obj
+.\Release\abcFanio.obj
+.\Release\abcFunc.obj
+.\Release\abcHie.obj
+.\Release\abcLatch.obj
+.\Release\abcLib.obj
+.\Release\abcMinBase.obj
+.\Release\abcNames.obj
+.\Release\abcNetlist.obj
+.\Release\abcNtk.obj
+.\Release\abcObj.obj
+.\Release\abcRefs.obj
+.\Release\abcShow.obj
+.\Release\abcSop.obj
+.\Release\abcUtil.obj
+.\Release\abc.obj
+.\Release\abcAttach.obj
+.\Release\abcAuto.obj
+.\Release\abcBalance.obj
+.\Release\abcBmc.obj
+.\Release\abcCas.obj
+.\Release\abcClpBdd.obj
+.\Release\abcClpSop.obj
+.\Release\abcCut.obj
+.\Release\abcDar.obj
+.\Release\abcDebug.obj
+.\Release\abcDress.obj
+.\Release\abcDsd.obj
+.\Release\abcEspresso.obj
+.\Release\abcExtract.obj
+.\Release\abcFpga.obj
+.\Release\abcFpgaFast.obj
+.\Release\abcFraig.obj
+.\Release\abcFxu.obj
+.\Release\abcGen.obj
+.\Release\abcHaig.obj
+.\Release\abcIf.obj
+.\Release\abcIvy.obj
+.\Release\abcLut.obj
+.\Release\abcMap.obj
+.\Release\abcMeasure.obj
+.\Release\abcMini.obj
+.\Release\abcMiter.obj
+.\Release\abcMulti.obj
+.\Release\abcMv.obj
+.\Release\abcNtbdd.obj
+.\Release\abcOdc.obj
+.\Release\abcOrder.obj
+.\Release\abcPart.obj
+.\Release\abcPrint.obj
+.\Release\abcProve.obj
+.\Release\abcQbf.obj
+.\Release\abcQuant.obj
+.\Release\abcRec.obj
+.\Release\abcReconv.obj
+.\Release\abcRefactor.obj
+.\Release\abcRenode.obj
+.\Release\abcReorder.obj
+.\Release\abcRestruct.obj
+.\Release\abcResub.obj
+.\Release\abcRewrite.obj
+.\Release\abcRr.obj
+.\Release\abcSat.obj
+.\Release\abcStrash.obj
+.\Release\abcSweep.obj
+.\Release\abcSymm.obj
+.\Release\abcTiming.obj
+.\Release\abcUnate.obj
+.\Release\abcUnreach.obj
+.\Release\abcVerify.obj
+.\Release\abcXsim.obj
+.\Release\cmd.obj
+.\Release\cmdAlias.obj
+.\Release\cmdApi.obj
+.\Release\cmdFlag.obj
+.\Release\cmdHist.obj
+.\Release\cmdUtils.obj
+.\Release\io.obj
+.\Release\ioReadAiger.obj
+.\Release\ioReadBaf.obj
+.\Release\ioReadBench.obj
+.\Release\ioReadBlif.obj
+.\Release\ioReadBlifAig.obj
+.\Release\ioReadBlifMv.obj
+.\Release\ioReadDsd.obj
+.\Release\ioReadEdif.obj
+.\Release\ioReadEqn.obj
+.\Release\ioReadPla.obj
+.\Release\ioReadVerilog.obj
+.\Release\ioUtil.obj
+.\Release\ioWriteAiger.obj
+.\Release\ioWriteBaf.obj
+.\Release\ioWriteBench.obj
+.\Release\ioWriteBlif.obj
+.\Release\ioWriteBlifMv.obj
+.\Release\ioWriteCnf.obj
+.\Release\ioWriteDot.obj
+.\Release\ioWriteEqn.obj
+.\Release\ioWriteGml.obj
+.\Release\ioWriteList.obj
+.\Release\ioWritePla.obj
+.\Release\ioWriteVerilog.obj
+.\Release\libSupport.obj
+.\Release\main.obj
+.\Release\mainFrame.obj
+.\Release\mainInit.obj
+.\Release\mainUtils.obj
+.\Release\verCore.obj
+.\Release\verFormula.obj
+.\Release\verParse.obj
+.\Release\verStream.obj
+.\Release\cuddAddAbs.obj
+.\Release\cuddAddApply.obj
+.\Release\cuddAddFind.obj
+.\Release\cuddAddInv.obj
+.\Release\cuddAddIte.obj
+.\Release\cuddAddNeg.obj
+.\Release\cuddAddWalsh.obj
+.\Release\cuddAndAbs.obj
+.\Release\cuddAnneal.obj
+.\Release\cuddApa.obj
+.\Release\cuddAPI.obj
+.\Release\cuddApprox.obj
+.\Release\cuddBddAbs.obj
+.\Release\cuddBddCorr.obj
+.\Release\cuddBddIte.obj
+.\Release\cuddBridge.obj
+.\Release\cuddCache.obj
+.\Release\cuddCheck.obj
+.\Release\cuddClip.obj
+.\Release\cuddCof.obj
+.\Release\cuddCompose.obj
+.\Release\cuddDecomp.obj
+.\Release\cuddEssent.obj
+.\Release\cuddExact.obj
+.\Release\cuddExport.obj
+.\Release\cuddGenCof.obj
+.\Release\cuddGenetic.obj
+.\Release\cuddGroup.obj
+.\Release\cuddHarwell.obj
+.\Release\cuddInit.obj
+.\Release\cuddInteract.obj
+.\Release\cuddLCache.obj
+.\Release\cuddLevelQ.obj
+.\Release\cuddLinear.obj
+.\Release\cuddLiteral.obj
+.\Release\cuddMatMult.obj
+.\Release\cuddPriority.obj
+.\Release\cuddRead.obj
+.\Release\cuddRef.obj
+.\Release\cuddReorder.obj
+.\Release\cuddSat.obj
+.\Release\cuddSign.obj
+.\Release\cuddSolve.obj
+.\Release\cuddSplit.obj
+.\Release\cuddSubsetHB.obj
+.\Release\cuddSubsetSP.obj
+.\Release\cuddSymmetry.obj
+.\Release\cuddTable.obj
+.\Release\cuddUtil.obj
+.\Release\cuddWindow.obj
+.\Release\cuddZddCount.obj
+.\Release\cuddZddFuncs.obj
+.\Release\cuddZddGroup.obj
+.\Release\cuddZddIsop.obj
+.\Release\cuddZddLin.obj
+.\Release\cuddZddMisc.obj
+.\Release\cuddZddPort.obj
+.\Release\cuddZddReord.obj
+.\Release\cuddZddSetop.obj
+.\Release\cuddZddSymm.obj
+.\Release\cuddZddUtil.obj
+.\Release\epd.obj
+.\Release\mtrBasic.obj
+.\Release\mtrGroup.obj
+.\Release\parseCore.obj
+.\Release\parseEqn.obj
+.\Release\parseStack.obj
+.\Release\dsdApi.obj
+.\Release\dsdCheck.obj
+.\Release\dsdLocal.obj
+.\Release\dsdMan.obj
+.\Release\dsdProc.obj
+.\Release\dsdTree.obj
+.\Release\reoApi.obj
+.\Release\reoCore.obj
+.\Release\reoProfile.obj
+.\Release\reoShuffle.obj
+.\Release\reoSift.obj
+.\Release\reoSwap.obj
+.\Release\reoTest.obj
+.\Release\reoTransfer.obj
+.\Release\reoUnits.obj
+.\Release\casCore.obj
+.\Release\casDec.obj
+.\Release\msatActivity.obj
+.\Release\msatClause.obj
+.\Release\msatClauseVec.obj
+.\Release\msatMem.obj
+.\Release\msatOrderH.obj
+.\Release\msatQueue.obj
+.\Release\msatRead.obj
+.\Release\msatSolverApi.obj
+.\Release\msatSolverCore.obj
+.\Release\msatSolverIo.obj
+.\Release\msatSolverSearch.obj
+.\Release\msatSort.obj
+.\Release\msatVec.obj
+.\Release\fraigApi.obj
+.\Release\fraigCanon.obj
+.\Release\fraigChoice.obj
+.\Release\fraigFanout.obj
+.\Release\fraigFeed.obj
+.\Release\fraigMan.obj
+.\Release\fraigMem.obj
+.\Release\fraigNode.obj
+.\Release\fraigPrime.obj
+.\Release\fraigSat.obj
+.\Release\fraigTable.obj
+.\Release\fraigUtil.obj
+.\Release\fraigVec.obj
+.\Release\csat_apis.obj
+.\Release\satInter.obj
+.\Release\satInterA.obj
+.\Release\satMem.obj
+.\Release\satSolver.obj
+.\Release\satStore.obj
+.\Release\satTrace.obj
+.\Release\satUtil.obj
+.\Release\pr.obj
+.\Release\fxu.obj
+.\Release\fxuCreate.obj
+.\Release\fxuHeapD.obj
+.\Release\fxuHeapS.obj
+.\Release\fxuList.obj
+.\Release\fxuMatrix.obj
+.\Release\fxuPair.obj
+.\Release\fxuPrint.obj
+.\Release\fxuReduce.obj
+.\Release\fxuSelect.obj
+.\Release\fxuSingle.obj
+.\Release\fxuUpdate.obj
+.\Release\rwrDec.obj
+.\Release\rwrEva.obj
+.\Release\rwrExp.obj
+.\Release\rwrLib.obj
+.\Release\rwrMan.obj
+.\Release\rwrPrint.obj
+.\Release\rwrTemp.obj
+.\Release\rwrUtil.obj
+.\Release\cutApi.obj
+.\Release\cutCut.obj
+.\Release\cutExpand.obj
+.\Release\cutMan.obj
+.\Release\cutMerge.obj
+.\Release\cutNode.obj
+.\Release\cutOracle.obj
+.\Release\cutPre22.obj
+.\Release\cutSeq.obj
+.\Release\cutTruth.obj
+.\Release\decAbc.obj
+.\Release\decFactor.obj
+.\Release\decMan.obj
+.\Release\decPrint.obj
+.\Release\decUtil.obj
+.\Release\simMan.obj
+.\Release\simSat.obj
+.\Release\simSeq.obj
+.\Release\simSupp.obj
+.\Release\simSwitch.obj
+.\Release\simSym.obj
+.\Release\simSymSat.obj
+.\Release\simSymSim.obj
+.\Release\simSymStr.obj
+.\Release\simUtils.obj
+.\Release\retArea.obj
+.\Release\retCore.obj
+.\Release\retDelay.obj
+.\Release\retFlow.obj
+.\Release\retIncrem.obj
+.\Release\retInit.obj
+.\Release\retLvalue.obj
+.\Release\resCore.obj
+.\Release\resDivs.obj
+.\Release\resFilter.obj
+.\Release\resSat.obj
+.\Release\resSim.obj
+.\Release\resStrash.obj
+.\Release\resWin.obj
+.\Release\lpkAbcDec.obj
+.\Release\lpkAbcDsd.obj
+.\Release\lpkAbcMux.obj
+.\Release\lpkAbcUtil.obj
+.\Release\lpkCore.obj
+.\Release\lpkCut.obj
+.\Release\lpkMan.obj
+.\Release\lpkMap.obj
+.\Release\lpkMulti.obj
+.\Release\lpkMux.obj
+.\Release\lpkSets.obj
+.\Release\fretFlow.obj
+.\Release\fretInit.obj
+.\Release\fretMain.obj
+.\Release\fretTime.obj
+.\Release\mfsCore.obj
+.\Release\mfsMan.obj
+.\Release\mfsSat.obj
+.\Release\mfsStrash.obj
+.\Release\mfsWin.obj
+.\Release\fpga.obj
+.\Release\fpgaCore.obj
+.\Release\fpgaCreate.obj
+.\Release\fpgaCut.obj
+.\Release\fpgaCutUtils.obj
+.\Release\fpgaFanout.obj
+.\Release\fpgaLib.obj
+.\Release\fpgaMatch.obj
+.\Release\fpgaSwitch.obj
+.\Release\fpgaTime.obj
+.\Release\fpgaTruth.obj
+.\Release\fpgaUtils.obj
+.\Release\fpgaVec.obj
+.\Release\mapper.obj
+.\Release\mapperCanon.obj
+.\Release\mapperCore.obj
+.\Release\mapperCreate.obj
+.\Release\mapperCut.obj
+.\Release\mapperCutUtils.obj
+.\Release\mapperFanout.obj
+.\Release\mapperLib.obj
+.\Release\mapperMatch.obj
+.\Release\mapperRefs.obj
+.\Release\mapperSuper.obj
+.\Release\mapperSwitch.obj
+.\Release\mapperTable.obj
+.\Release\mapperTime.obj
+.\Release\mapperTree.obj
+.\Release\mapperTruth.obj
+.\Release\mapperUtils.obj
+.\Release\mapperVec.obj
+.\Release\mio.obj
+.\Release\mioApi.obj
+.\Release\mioFunc.obj
+.\Release\mioRead.obj
+.\Release\mioUtils.obj
+.\Release\super.obj
+.\Release\superAnd.obj
+.\Release\superGate.obj
+.\Release\superWrite.obj
+.\Release\ifCore.obj
+.\Release\ifCut.obj
+.\Release\ifMan.obj
+.\Release\ifMap.obj
+.\Release\ifReduce.obj
+.\Release\ifTime.obj
+.\Release\ifTruth.obj
+.\Release\ifUtil.obj
+.\Release\pcmCore.obj
+.\Release\pcmCut.obj
+.\Release\pcmMan.obj
+.\Release\pcmMap.obj
+.\Release\pcmReduce.obj
+.\Release\pcmTime.obj
+.\Release\pcmTruth.obj
+.\Release\pcmUtil.obj
+.\Release\plyAbc.obj
+.\Release\plyAig.obj
+.\Release\plyIter.obj
+.\Release\plyLib.obj
+.\Release\plyMan.obj
+.\Release\plyMap.obj
+.\Release\plyNtk.obj
+.\Release\plyPar.obj
+.\Release\extraBddAuto.obj
+.\Release\extraBddCas.obj
+.\Release\extraBddKmap.obj
+.\Release\extraBddMisc.obj
+.\Release\extraBddSymm.obj
+.\Release\extraBddUnate.obj
+.\Release\extraUtilBitMatrix.obj
+.\Release\extraUtilCanon.obj
+.\Release\extraUtilFile.obj
+.\Release\extraUtilMemory.obj
+.\Release\extraUtilMisc.obj
+.\Release\extraUtilProgress.obj
+.\Release\extraUtilReader.obj
+.\Release\extraUtilTruth.obj
+.\Release\extraUtilUtil.obj
+.\Release\st.obj
+.\Release\stmm.obj
+.\Release\mvc.obj
+.\Release\mvcApi.obj
+.\Release\mvcCompare.obj
+.\Release\mvcContain.obj
+.\Release\mvcCover.obj
+.\Release\mvcCube.obj
+.\Release\mvcDivide.obj
+.\Release\mvcDivisor.obj
+.\Release\mvcList.obj
+.\Release\mvcLits.obj
+.\Release\mvcMan.obj
+.\Release\mvcOpAlg.obj
+.\Release\mvcOpBool.obj
+.\Release\mvcPrint.obj
+.\Release\mvcSort.obj
+.\Release\mvcUtils.obj
+.\Release\cofactor.obj
+.\Release\cols.obj
+.\Release\compl.obj
+.\Release\contain.obj
+.\Release\cubehack.obj
+.\Release\cubestr.obj
+.\Release\cvrin.obj
+.\Release\cvrm.obj
+.\Release\cvrmisc.obj
+.\Release\cvrout.obj
+.\Release\dominate.obj
+.\Release\equiv.obj
+.\Release\espresso.obj
+.\Release\essen.obj
+.\Release\exact.obj
+.\Release\expand.obj
+.\Release\gasp.obj
+.\Release\gimpel.obj
+.\Release\globals.obj
+.\Release\hack.obj
+.\Release\indep.obj
+.\Release\irred.obj
+.\Release\map.obj
+.\Release\matrix.obj
+.\Release\mincov.obj
+.\Release\opo.obj
+.\Release\pair.obj
+.\Release\part.obj
+.\Release\primes.obj
+.\Release\reduce.obj
+.\Release\rows.obj
+.\Release\set.obj
+.\Release\setc.obj
+.\Release\sharp.obj
+.\Release\sminterf.obj
+.\Release\solution.obj
+.\Release\sparse.obj
+.\Release\unate.obj
+.\Release\verify.obj
+.\Release\nmApi.obj
+.\Release\nmTable.obj
+.\Release\hopBalance.obj
+.\Release\hopCheck.obj
+.\Release\hopDfs.obj
+.\Release\hopMan.obj
+.\Release\hopMem.obj
+.\Release\hopObj.obj
+.\Release\hopOper.obj
+.\Release\hopTable.obj
+.\Release\hopUtil.obj
+.\Release\ivyBalance.obj
+.\Release\ivyCanon.obj
+.\Release\ivyCheck.obj
+.\Release\ivyCut.obj
+.\Release\ivyCutTrav.obj
+.\Release\ivyDfs.obj
+.\Release\ivyDsd.obj
+.\Release\ivyFanout.obj
+.\Release\ivyFastMap.obj
+.\Release\ivyFraig.obj
+.\Release\ivyHaig.obj
+.\Release\ivyMan.obj
+.\Release\ivyMem.obj
+.\Release\ivyMulti.obj
+.\Release\ivyObj.obj
+.\Release\ivyOper.obj
+.\Release\ivyResyn.obj
+.\Release\ivyRwr.obj
+.\Release\ivySeq.obj
+.\Release\ivyShow.obj
+.\Release\ivyTable.obj
+.\Release\ivyUtil.obj
+.\Release\rwtDec.obj
+.\Release\rwtMan.obj
+.\Release\rwtUtil.obj
+.\Release\mem.obj
+.\Release\ioaReadAig.obj
+.\Release\ioaUtil.obj
+.\Release\ioaWriteAig.obj
+.\Release\darBalance.obj
+.\Release\darCore.obj
+.\Release\darCut.obj
+.\Release\darData.obj
+.\Release\darLib.obj
+.\Release\darMan.obj
+.\Release\darPrec.obj
+.\Release\darRefact.obj
+.\Release\darResub.obj
+.\Release\darScript.obj
+.\Release\fraBmc.obj
+.\Release\fraCec.obj
+.\Release\fraClass.obj
+.\Release\fraClau.obj
+.\Release\fraClaus.obj
+.\Release\fraCnf.obj
+.\Release\fraCore.obj
+.\Release\fraHot.obj
+.\Release\fraImp.obj
+.\Release\fraInd.obj
+.\Release\fraIndVer.obj
+.\Release\fraLcr.obj
+.\Release\fraMan.obj
+.\Release\fraPart.obj
+.\Release\fraSat.obj
+.\Release\fraSec.obj
+.\Release\fraSim.obj
+.\Release\cnfCore.obj
+.\Release\cnfCut.obj
+.\Release\cnfData.obj
+.\Release\cnfMan.obj
+.\Release\cnfMap.obj
+.\Release\cnfPost.obj
+.\Release\cnfUtil.obj
+.\Release\cnfWrite.obj
+.\Release\cswCore.obj
+.\Release\cswCut.obj
+.\Release\cswMan.obj
+.\Release\cswTable.obj
+.\Release\cloud.obj
+.\Release\kitAig.obj
+.\Release\kitBdd.obj
+.\Release\kitCloud.obj
+.\Release\kitDsd.obj
+.\Release\kitFactor.obj
+.\Release\kitGraph.obj
+.\Release\kitHop.obj
+.\Release\kitIsop.obj
+.\Release\kitSop.obj
+.\Release\kitTruth.obj
+.\Release\bdcCore.obj
+.\Release\bdcDec.obj
+.\Release\bdcTable.obj
+.\Release\aigCheck.obj
+.\Release\aigCuts.obj
+.\Release\aigDfs.obj
+.\Release\aigFanout.obj
+.\Release\aigFrames.obj
+.\Release\aigHaig.obj
+.\Release\aigInter.obj
+.\Release\aigMan.obj
+.\Release\aigMem.obj
+.\Release\aigMffc.obj
+.\Release\aigObj.obj
+.\Release\aigOper.obj
+.\Release\aigOrder.obj
+.\Release\aigPart.obj
+.\Release\aigRepr.obj
+.\Release\aigRet.obj
+.\Release\aigRetF.obj
+.\Release\aigScl.obj
+.\Release\aigSeq.obj
+.\Release\aigShow.obj
+.\Release\aigTable.obj
+.\Release\aigTiming.obj
+.\Release\aigTruth.obj
+.\Release\aigTsim.obj
+.\Release\aigUtil.obj
+.\Release\aigWin.obj
+.\Release\bar.obj
+.\Release\ntlAig.obj
+.\Release\ntlCheck.obj
+.\Release\ntlDfs.obj
+.\Release\ntlMan.obj
+.\Release\ntlMap.obj
+.\Release\ntlObj.obj
+.\Release\ntlReadBlif.obj
+.\Release\ntlTable.obj
+.\Release\ntlTime.obj
+.\Release\ntlWriteBlif.obj
+.\Release\tim.obj
+.\Release\mfsDiv.obj
+.\Release\mfsResub.obj
+.\Release\mfsInter.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB42.tmp"
+<h3>Output Window</h3>
+Compiling...
+mfsMan.c
+Linking...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB44.tmp" with contents
+[
+/nologo /o"Release/abc.bsc" 
+.\Release\abcAig.sbr
+.\Release\abcBlifMv.sbr
+.\Release\abcCheck.sbr
+.\Release\abcDfs.sbr
+.\Release\abcFanio.sbr
+.\Release\abcFunc.sbr
+.\Release\abcHie.sbr
+.\Release\abcLatch.sbr
+.\Release\abcLib.sbr
+.\Release\abcMinBase.sbr
+.\Release\abcNames.sbr
+.\Release\abcNetlist.sbr
+.\Release\abcNtk.sbr
+.\Release\abcObj.sbr
+.\Release\abcRefs.sbr
+.\Release\abcShow.sbr
+.\Release\abcSop.sbr
+.\Release\abcUtil.sbr
+.\Release\abc.sbr
+.\Release\abcAttach.sbr
+.\Release\abcAuto.sbr
+.\Release\abcBalance.sbr
+.\Release\abcBmc.sbr
+.\Release\abcCas.sbr
+.\Release\abcClpBdd.sbr
+.\Release\abcClpSop.sbr
+.\Release\abcCut.sbr
+.\Release\abcDar.sbr
+.\Release\abcDebug.sbr
+.\Release\abcDress.sbr
+.\Release\abcDsd.sbr
+.\Release\abcEspresso.sbr
+.\Release\abcExtract.sbr
+.\Release\abcFpga.sbr
+.\Release\abcFpgaFast.sbr
+.\Release\abcFraig.sbr
+.\Release\abcFxu.sbr
+.\Release\abcGen.sbr
+.\Release\abcHaig.sbr
+.\Release\abcIf.sbr
+.\Release\abcIvy.sbr
+.\Release\abcLut.sbr
+.\Release\abcMap.sbr
+.\Release\abcMeasure.sbr
+.\Release\abcMini.sbr
+.\Release\abcMiter.sbr
+.\Release\abcMulti.sbr
+.\Release\abcMv.sbr
+.\Release\abcNtbdd.sbr
+.\Release\abcOdc.sbr
+.\Release\abcOrder.sbr
+.\Release\abcPart.sbr
+.\Release\abcPrint.sbr
+.\Release\abcProve.sbr
+.\Release\abcQbf.sbr
+.\Release\abcQuant.sbr
+.\Release\abcRec.sbr
+.\Release\abcReconv.sbr
+.\Release\abcRefactor.sbr
+.\Release\abcRenode.sbr
+.\Release\abcReorder.sbr
+.\Release\abcRestruct.sbr
+.\Release\abcResub.sbr
+.\Release\abcRewrite.sbr
+.\Release\abcRr.sbr
+.\Release\abcSat.sbr
+.\Release\abcStrash.sbr
+.\Release\abcSweep.sbr
+.\Release\abcSymm.sbr
+.\Release\abcTiming.sbr
+.\Release\abcUnate.sbr
+.\Release\abcUnreach.sbr
+.\Release\abcVerify.sbr
+.\Release\abcXsim.sbr
+.\Release\cmd.sbr
+.\Release\cmdAlias.sbr
+.\Release\cmdApi.sbr
+.\Release\cmdFlag.sbr
+.\Release\cmdHist.sbr
+.\Release\cmdUtils.sbr
+.\Release\io.sbr
+.\Release\ioReadAiger.sbr
+.\Release\ioReadBaf.sbr
+.\Release\ioReadBench.sbr
+.\Release\ioReadBlif.sbr
+.\Release\ioReadBlifAig.sbr
+.\Release\ioReadBlifMv.sbr
+.\Release\ioReadDsd.sbr
+.\Release\ioReadEdif.sbr
+.\Release\ioReadEqn.sbr
+.\Release\ioReadPla.sbr
+.\Release\ioReadVerilog.sbr
+.\Release\ioUtil.sbr
+.\Release\ioWriteAiger.sbr
+.\Release\ioWriteBaf.sbr
+.\Release\ioWriteBench.sbr
+.\Release\ioWriteBlif.sbr
+.\Release\ioWriteBlifMv.sbr
+.\Release\ioWriteCnf.sbr
+.\Release\ioWriteDot.sbr
+.\Release\ioWriteEqn.sbr
+.\Release\ioWriteGml.sbr
+.\Release\ioWriteList.sbr
+.\Release\ioWritePla.sbr
+.\Release\ioWriteVerilog.sbr
+.\Release\libSupport.sbr
+.\Release\main.sbr
+.\Release\mainFrame.sbr
+.\Release\mainInit.sbr
+.\Release\mainUtils.sbr
+.\Release\verCore.sbr
+.\Release\verFormula.sbr
+.\Release\verParse.sbr
+.\Release\verStream.sbr
+.\Release\cuddAddAbs.sbr
+.\Release\cuddAddApply.sbr
+.\Release\cuddAddFind.sbr
+.\Release\cuddAddInv.sbr
+.\Release\cuddAddIte.sbr
+.\Release\cuddAddNeg.sbr
+.\Release\cuddAddWalsh.sbr
+.\Release\cuddAndAbs.sbr
+.\Release\cuddAnneal.sbr
+.\Release\cuddApa.sbr
+.\Release\cuddAPI.sbr
+.\Release\cuddApprox.sbr
+.\Release\cuddBddAbs.sbr
+.\Release\cuddBddCorr.sbr
+.\Release\cuddBddIte.sbr
+.\Release\cuddBridge.sbr
+.\Release\cuddCache.sbr
+.\Release\cuddCheck.sbr
+.\Release\cuddClip.sbr
+.\Release\cuddCof.sbr
+.\Release\cuddCompose.sbr
+.\Release\cuddDecomp.sbr
+.\Release\cuddEssent.sbr
+.\Release\cuddExact.sbr
+.\Release\cuddExport.sbr
+.\Release\cuddGenCof.sbr
+.\Release\cuddGenetic.sbr
+.\Release\cuddGroup.sbr
+.\Release\cuddHarwell.sbr
+.\Release\cuddInit.sbr
+.\Release\cuddInteract.sbr
+.\Release\cuddLCache.sbr
+.\Release\cuddLevelQ.sbr
+.\Release\cuddLinear.sbr
+.\Release\cuddLiteral.sbr
+.\Release\cuddMatMult.sbr
+.\Release\cuddPriority.sbr
+.\Release\cuddRead.sbr
+.\Release\cuddRef.sbr
+.\Release\cuddReorder.sbr
+.\Release\cuddSat.sbr
+.\Release\cuddSign.sbr
+.\Release\cuddSolve.sbr
+.\Release\cuddSplit.sbr
+.\Release\cuddSubsetHB.sbr
+.\Release\cuddSubsetSP.sbr
+.\Release\cuddSymmetry.sbr
+.\Release\cuddTable.sbr
+.\Release\cuddUtil.sbr
+.\Release\cuddWindow.sbr
+.\Release\cuddZddCount.sbr
+.\Release\cuddZddFuncs.sbr
+.\Release\cuddZddGroup.sbr
+.\Release\cuddZddIsop.sbr
+.\Release\cuddZddLin.sbr
+.\Release\cuddZddMisc.sbr
+.\Release\cuddZddPort.sbr
+.\Release\cuddZddReord.sbr
+.\Release\cuddZddSetop.sbr
+.\Release\cuddZddSymm.sbr
+.\Release\cuddZddUtil.sbr
+.\Release\epd.sbr
+.\Release\mtrBasic.sbr
+.\Release\mtrGroup.sbr
+.\Release\parseCore.sbr
+.\Release\parseEqn.sbr
+.\Release\parseStack.sbr
+.\Release\dsdApi.sbr
+.\Release\dsdCheck.sbr
+.\Release\dsdLocal.sbr
+.\Release\dsdMan.sbr
+.\Release\dsdProc.sbr
+.\Release\dsdTree.sbr
+.\Release\reoApi.sbr
+.\Release\reoCore.sbr
+.\Release\reoProfile.sbr
+.\Release\reoShuffle.sbr
+.\Release\reoSift.sbr
+.\Release\reoSwap.sbr
+.\Release\reoTest.sbr
+.\Release\reoTransfer.sbr
+.\Release\reoUnits.sbr
+.\Release\casCore.sbr
+.\Release\casDec.sbr
+.\Release\msatActivity.sbr
+.\Release\msatClause.sbr
+.\Release\msatClauseVec.sbr
+.\Release\msatMem.sbr
+.\Release\msatOrderH.sbr
+.\Release\msatQueue.sbr
+.\Release\msatRead.sbr
+.\Release\msatSolverApi.sbr
+.\Release\msatSolverCore.sbr
+.\Release\msatSolverIo.sbr
+.\Release\msatSolverSearch.sbr
+.\Release\msatSort.sbr
+.\Release\msatVec.sbr
+.\Release\fraigApi.sbr
+.\Release\fraigCanon.sbr
+.\Release\fraigChoice.sbr
+.\Release\fraigFanout.sbr
+.\Release\fraigFeed.sbr
+.\Release\fraigMan.sbr
+.\Release\fraigMem.sbr
+.\Release\fraigNode.sbr
+.\Release\fraigPrime.sbr
+.\Release\fraigSat.sbr
+.\Release\fraigTable.sbr
+.\Release\fraigUtil.sbr
+.\Release\fraigVec.sbr
+.\Release\csat_apis.sbr
+.\Release\satInter.sbr
+.\Release\satInterA.sbr
+.\Release\satMem.sbr
+.\Release\satSolver.sbr
+.\Release\satStore.sbr
+.\Release\satTrace.sbr
+.\Release\satUtil.sbr
+.\Release\pr.sbr
+.\Release\fxu.sbr
+.\Release\fxuCreate.sbr
+.\Release\fxuHeapD.sbr
+.\Release\fxuHeapS.sbr
+.\Release\fxuList.sbr
+.\Release\fxuMatrix.sbr
+.\Release\fxuPair.sbr
+.\Release\fxuPrint.sbr
+.\Release\fxuReduce.sbr
+.\Release\fxuSelect.sbr
+.\Release\fxuSingle.sbr
+.\Release\fxuUpdate.sbr
+.\Release\rwrDec.sbr
+.\Release\rwrEva.sbr
+.\Release\rwrExp.sbr
+.\Release\rwrLib.sbr
+.\Release\rwrMan.sbr
+.\Release\rwrPrint.sbr
+.\Release\rwrTemp.sbr
+.\Release\rwrUtil.sbr
+.\Release\cutApi.sbr
+.\Release\cutCut.sbr
+.\Release\cutExpand.sbr
+.\Release\cutMan.sbr
+.\Release\cutMerge.sbr
+.\Release\cutNode.sbr
+.\Release\cutOracle.sbr
+.\Release\cutPre22.sbr
+.\Release\cutSeq.sbr
+.\Release\cutTruth.sbr
+.\Release\decAbc.sbr
+.\Release\decFactor.sbr
+.\Release\decMan.sbr
+.\Release\decPrint.sbr
+.\Release\decUtil.sbr
+.\Release\simMan.sbr
+.\Release\simSat.sbr
+.\Release\simSeq.sbr
+.\Release\simSupp.sbr
+.\Release\simSwitch.sbr
+.\Release\simSym.sbr
+.\Release\simSymSat.sbr
+.\Release\simSymSim.sbr
+.\Release\simSymStr.sbr
+.\Release\simUtils.sbr
+.\Release\retArea.sbr
+.\Release\retCore.sbr
+.\Release\retDelay.sbr
+.\Release\retFlow.sbr
+.\Release\retIncrem.sbr
+.\Release\retInit.sbr
+.\Release\retLvalue.sbr
+.\Release\resCore.sbr
+.\Release\resDivs.sbr
+.\Release\resFilter.sbr
+.\Release\resSat.sbr
+.\Release\resSim.sbr
+.\Release\resStrash.sbr
+.\Release\resWin.sbr
+.\Release\lpkAbcDec.sbr
+.\Release\lpkAbcDsd.sbr
+.\Release\lpkAbcMux.sbr
+.\Release\lpkAbcUtil.sbr
+.\Release\lpkCore.sbr
+.\Release\lpkCut.sbr
+.\Release\lpkMan.sbr
+.\Release\lpkMap.sbr
+.\Release\lpkMulti.sbr
+.\Release\lpkMux.sbr
+.\Release\lpkSets.sbr
+.\Release\fretFlow.sbr
+.\Release\fretInit.sbr
+.\Release\fretMain.sbr
+.\Release\fretTime.sbr
+.\Release\mfsCore.sbr
+.\Release\mfsMan.sbr
+.\Release\mfsSat.sbr
+.\Release\mfsStrash.sbr
+.\Release\mfsWin.sbr
+.\Release\fpga.sbr
+.\Release\fpgaCore.sbr
+.\Release\fpgaCreate.sbr
+.\Release\fpgaCut.sbr
+.\Release\fpgaCutUtils.sbr
+.\Release\fpgaFanout.sbr
+.\Release\fpgaLib.sbr
+.\Release\fpgaMatch.sbr
+.\Release\fpgaSwitch.sbr
+.\Release\fpgaTime.sbr
+.\Release\fpgaTruth.sbr
+.\Release\fpgaUtils.sbr
+.\Release\fpgaVec.sbr
+.\Release\mapper.sbr
+.\Release\mapperCanon.sbr
+.\Release\mapperCore.sbr
+.\Release\mapperCreate.sbr
+.\Release\mapperCut.sbr
+.\Release\mapperCutUtils.sbr
+.\Release\mapperFanout.sbr
+.\Release\mapperLib.sbr
+.\Release\mapperMatch.sbr
+.\Release\mapperRefs.sbr
+.\Release\mapperSuper.sbr
+.\Release\mapperSwitch.sbr
+.\Release\mapperTable.sbr
+.\Release\mapperTime.sbr
+.\Release\mapperTree.sbr
+.\Release\mapperTruth.sbr
+.\Release\mapperUtils.sbr
+.\Release\mapperVec.sbr
+.\Release\mio.sbr
+.\Release\mioApi.sbr
+.\Release\mioFunc.sbr
+.\Release\mioRead.sbr
+.\Release\mioUtils.sbr
+.\Release\super.sbr
+.\Release\superAnd.sbr
+.\Release\superGate.sbr
+.\Release\superWrite.sbr
+.\Release\ifCore.sbr
+.\Release\ifCut.sbr
+.\Release\ifMan.sbr
+.\Release\ifMap.sbr
+.\Release\ifReduce.sbr
+.\Release\ifTime.sbr
+.\Release\ifTruth.sbr
+.\Release\ifUtil.sbr
+.\Release\pcmCore.sbr
+.\Release\pcmCut.sbr
+.\Release\pcmMan.sbr
+.\Release\pcmMap.sbr
+.\Release\pcmReduce.sbr
+.\Release\pcmTime.sbr
+.\Release\pcmTruth.sbr
+.\Release\pcmUtil.sbr
+.\Release\plyAbc.sbr
+.\Release\plyAig.sbr
+.\Release\plyIter.sbr
+.\Release\plyLib.sbr
+.\Release\plyMan.sbr
+.\Release\plyMap.sbr
+.\Release\plyNtk.sbr
+.\Release\plyPar.sbr
+.\Release\extraBddAuto.sbr
+.\Release\extraBddCas.sbr
+.\Release\extraBddKmap.sbr
+.\Release\extraBddMisc.sbr
+.\Release\extraBddSymm.sbr
+.\Release\extraBddUnate.sbr
+.\Release\extraUtilBitMatrix.sbr
+.\Release\extraUtilCanon.sbr
+.\Release\extraUtilFile.sbr
+.\Release\extraUtilMemory.sbr
+.\Release\extraUtilMisc.sbr
+.\Release\extraUtilProgress.sbr
+.\Release\extraUtilReader.sbr
+.\Release\extraUtilTruth.sbr
+.\Release\extraUtilUtil.sbr
+.\Release\st.sbr
+.\Release\stmm.sbr
+.\Release\mvc.sbr
+.\Release\mvcApi.sbr
+.\Release\mvcCompare.sbr
+.\Release\mvcContain.sbr
+.\Release\mvcCover.sbr
+.\Release\mvcCube.sbr
+.\Release\mvcDivide.sbr
+.\Release\mvcDivisor.sbr
+.\Release\mvcList.sbr
+.\Release\mvcLits.sbr
+.\Release\mvcMan.sbr
+.\Release\mvcOpAlg.sbr
+.\Release\mvcOpBool.sbr
+.\Release\mvcPrint.sbr
+.\Release\mvcSort.sbr
+.\Release\mvcUtils.sbr
+.\Release\cofactor.sbr
+.\Release\cols.sbr
+.\Release\compl.sbr
+.\Release\contain.sbr
+.\Release\cubehack.sbr
+.\Release\cubestr.sbr
+.\Release\cvrin.sbr
+.\Release\cvrm.sbr
+.\Release\cvrmisc.sbr
+.\Release\cvrout.sbr
+.\Release\dominate.sbr
+.\Release\equiv.sbr
+.\Release\espresso.sbr
+.\Release\essen.sbr
+.\Release\exact.sbr
+.\Release\expand.sbr
+.\Release\gasp.sbr
+.\Release\gimpel.sbr
+.\Release\globals.sbr
+.\Release\hack.sbr
+.\Release\indep.sbr
+.\Release\irred.sbr
+.\Release\map.sbr
+.\Release\matrix.sbr
+.\Release\mincov.sbr
+.\Release\opo.sbr
+.\Release\pair.sbr
+.\Release\part.sbr
+.\Release\primes.sbr
+.\Release\reduce.sbr
+.\Release\rows.sbr
+.\Release\set.sbr
+.\Release\setc.sbr
+.\Release\sharp.sbr
+.\Release\sminterf.sbr
+.\Release\solution.sbr
+.\Release\sparse.sbr
+.\Release\unate.sbr
+.\Release\verify.sbr
+.\Release\nmApi.sbr
+.\Release\nmTable.sbr
+.\Release\hopBalance.sbr
+.\Release\hopCheck.sbr
+.\Release\hopDfs.sbr
+.\Release\hopMan.sbr
+.\Release\hopMem.sbr
+.\Release\hopObj.sbr
+.\Release\hopOper.sbr
+.\Release\hopTable.sbr
+.\Release\hopUtil.sbr
+.\Release\ivyBalance.sbr
+.\Release\ivyCanon.sbr
+.\Release\ivyCheck.sbr
+.\Release\ivyCut.sbr
+.\Release\ivyCutTrav.sbr
+.\Release\ivyDfs.sbr
+.\Release\ivyDsd.sbr
+.\Release\ivyFanout.sbr
+.\Release\ivyFastMap.sbr
+.\Release\ivyFraig.sbr
+.\Release\ivyHaig.sbr
+.\Release\ivyMan.sbr
+.\Release\ivyMem.sbr
+.\Release\ivyMulti.sbr
+.\Release\ivyObj.sbr
+.\Release\ivyOper.sbr
+.\Release\ivyResyn.sbr
+.\Release\ivyRwr.sbr
+.\Release\ivySeq.sbr
+.\Release\ivyShow.sbr
+.\Release\ivyTable.sbr
+.\Release\ivyUtil.sbr
+.\Release\rwtDec.sbr
+.\Release\rwtMan.sbr
+.\Release\rwtUtil.sbr
+.\Release\mem.sbr
+.\Release\ioaReadAig.sbr
+.\Release\ioaUtil.sbr
+.\Release\ioaWriteAig.sbr
+.\Release\darBalance.sbr
+.\Release\darCore.sbr
+.\Release\darCut.sbr
+.\Release\darData.sbr
+.\Release\darLib.sbr
+.\Release\darMan.sbr
+.\Release\darPrec.sbr
+.\Release\darRefact.sbr
+.\Release\darResub.sbr
+.\Release\darScript.sbr
+.\Release\fraBmc.sbr
+.\Release\fraCec.sbr
+.\Release\fraClass.sbr
+.\Release\fraClau.sbr
+.\Release\fraClaus.sbr
+.\Release\fraCnf.sbr
+.\Release\fraCore.sbr
+.\Release\fraHot.sbr
+.\Release\fraImp.sbr
+.\Release\fraInd.sbr
+.\Release\fraIndVer.sbr
+.\Release\fraLcr.sbr
+.\Release\fraMan.sbr
+.\Release\fraPart.sbr
+.\Release\fraSat.sbr
+.\Release\fraSec.sbr
+.\Release\fraSim.sbr
+.\Release\cnfCore.sbr
+.\Release\cnfCut.sbr
+.\Release\cnfData.sbr
+.\Release\cnfMan.sbr
+.\Release\cnfMap.sbr
+.\Release\cnfPost.sbr
+.\Release\cnfUtil.sbr
+.\Release\cnfWrite.sbr
+.\Release\cswCore.sbr
+.\Release\cswCut.sbr
+.\Release\cswMan.sbr
+.\Release\cswTable.sbr
+.\Release\cloud.sbr
+.\Release\kitAig.sbr
+.\Release\kitBdd.sbr
+.\Release\kitCloud.sbr
+.\Release\kitDsd.sbr
+.\Release\kitFactor.sbr
+.\Release\kitGraph.sbr
+.\Release\kitHop.sbr
+.\Release\kitIsop.sbr
+.\Release\kitSop.sbr
+.\Release\kitTruth.sbr
+.\Release\bdcCore.sbr
+.\Release\bdcDec.sbr
+.\Release\bdcTable.sbr
+.\Release\aigCheck.sbr
+.\Release\aigCuts.sbr
+.\Release\aigDfs.sbr
+.\Release\aigFanout.sbr
+.\Release\aigFrames.sbr
+.\Release\aigHaig.sbr
+.\Release\aigInter.sbr
+.\Release\aigMan.sbr
+.\Release\aigMem.sbr
+.\Release\aigMffc.sbr
+.\Release\aigObj.sbr
+.\Release\aigOper.sbr
+.\Release\aigOrder.sbr
+.\Release\aigPart.sbr
+.\Release\aigRepr.sbr
+.\Release\aigRet.sbr
+.\Release\aigRetF.sbr
+.\Release\aigScl.sbr
+.\Release\aigSeq.sbr
+.\Release\aigShow.sbr
+.\Release\aigTable.sbr
+.\Release\aigTiming.sbr
+.\Release\aigTruth.sbr
+.\Release\aigTsim.sbr
+.\Release\aigUtil.sbr
+.\Release\aigWin.sbr
+.\Release\bar.sbr
+.\Release\ntlAig.sbr
+.\Release\ntlCheck.sbr
+.\Release\ntlDfs.sbr
+.\Release\ntlMan.sbr
+.\Release\ntlMap.sbr
+.\Release\ntlObj.sbr
+.\Release\ntlReadBlif.sbr
+.\Release\ntlTable.sbr
+.\Release\ntlTime.sbr
+.\Release\ntlWriteBlif.sbr
+.\Release\tim.sbr
+.\Release\mfsDiv.sbr
+.\Release\mfsResub.sbr
+.\Release\mfsInter.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPB44.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abc.exe - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>
diff --git a/abclib.plg b/abclib.plg
new file mode 100644
index 00000000..b346e07b
--- /dev/null
+++ b/abclib.plg
@@ -0,0 +1,2208 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abclib - Win32 Debug--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AB.tmp" with contents
+[
+/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"abclib\DebugLib/" /Fp"abclib\DebugLib/abclib.pch" /YX /Fo"abclib\DebugLib/" /Fd"abclib\DebugLib/" /FD /GZ /c 
+"C:\_projects\abc\src\base\abc\abcAig.c"
+"C:\_projects\abc\src\base\abc\abcCheck.c"
+"C:\_projects\abc\src\base\abc\abcDfs.c"
+"C:\_projects\abc\src\base\abc\abcFanio.c"
+"C:\_projects\abc\src\base\abc\abcFunc.c"
+"C:\_projects\abc\src\base\abc\abcLatch.c"
+"C:\_projects\abc\src\base\abc\abcLib.c"
+"C:\_projects\abc\src\base\abc\abcMinBase.c"
+"C:\_projects\abc\src\base\abc\abcNames.c"
+"C:\_projects\abc\src\base\abc\abcNetlist.c"
+"C:\_projects\abc\src\base\abc\abcNtk.c"
+"C:\_projects\abc\src\base\abc\abcObj.c"
+"C:\_projects\abc\src\base\abc\abcRefs.c"
+"C:\_projects\abc\src\base\abc\abcShow.c"
+"C:\_projects\abc\src\base\abc\abcSop.c"
+"C:\_projects\abc\src\base\abc\abcUtil.c"
+"C:\_projects\abc\src\base\abci\abc.c"
+"C:\_projects\abc\src\base\abci\abcAttach.c"
+"C:\_projects\abc\src\base\abci\abcAuto.c"
+"C:\_projects\abc\src\base\abci\abcBalance.c"
+"C:\_projects\abc\src\base\abci\abcBmc.c"
+"C:\_projects\abc\src\base\abci\abcClpBdd.c"
+"C:\_projects\abc\src\base\abci\abcClpSop.c"
+"C:\_projects\abc\src\base\abci\abcCut.c"
+"C:\_projects\abc\src\base\abci\abcDebug.c"
+"C:\_projects\abc\src\base\abci\abcDress.c"
+"C:\_projects\abc\src\base\abci\abcDsd.c"
+"C:\_projects\abc\src\base\abci\abcEspresso.c"
+"C:\_projects\abc\src\base\abci\abcExtract.c"
+"C:\_projects\abc\src\base\abci\abcFpga.c"
+"C:\_projects\abc\src\base\abci\abcFpgaFast.c"
+"C:\_projects\abc\src\base\abci\abcFraig.c"
+"C:\_projects\abc\src\base\abci\abcFxu.c"
+"C:\_projects\abc\src\base\abci\abcGen.c"
+"C:\_projects\abc\src\base\abci\abcIf.c"
+"C:\_projects\abc\src\base\abci\abcIvy.c"
+"C:\_projects\abc\src\base\abci\abcLut.c"
+"C:\_projects\abc\src\base\abci\abcMap.c"
+"C:\_projects\abc\src\base\abci\abcMini.c"
+"C:\_projects\abc\src\base\abci\abcMiter.c"
+"C:\_projects\abc\src\base\abci\abcMulti.c"
+"C:\_projects\abc\src\base\abci\abcMv.c"
+"C:\_projects\abc\src\base\abci\abcNtbdd.c"
+"C:\_projects\abc\src\base\abci\abcOrder.c"
+"C:\_projects\abc\src\base\abci\abcPrint.c"
+"C:\_projects\abc\src\base\abci\abcProve.c"
+"C:\_projects\abc\src\base\abci\abcReconv.c"
+"C:\_projects\abc\src\base\abci\abcRefactor.c"
+"C:\_projects\abc\src\base\abci\abcRenode.c"
+"C:\_projects\abc\src\base\abci\abcReorder.c"
+"C:\_projects\abc\src\base\abci\abcRestruct.c"
+"C:\_projects\abc\src\base\abci\abcResub.c"
+"C:\_projects\abc\src\base\abci\abcRewrite.c"
+"C:\_projects\abc\src\base\abci\abcRr.c"
+"C:\_projects\abc\src\base\abci\abcSat.c"
+"C:\_projects\abc\src\base\abci\abcStrash.c"
+"C:\_projects\abc\src\base\abci\abcSweep.c"
+"C:\_projects\abc\src\base\abci\abcSymm.c"
+"C:\_projects\abc\src\base\abci\abcTiming.c"
+"C:\_projects\abc\src\base\abci\abcUnate.c"
+"C:\_projects\abc\src\base\abci\abcUnreach.c"
+"C:\_projects\abc\src\base\abci\abcVerify.c"
+"C:\_projects\abc\src\base\abci\abcXsim.c"
+"C:\_projects\abc\src\base\cmd\cmd.c"
+"C:\_projects\abc\src\base\cmd\cmdAlias.c"
+"C:\_projects\abc\src\base\cmd\cmdApi.c"
+"C:\_projects\abc\src\base\cmd\cmdFlag.c"
+"C:\_projects\abc\src\base\cmd\cmdHist.c"
+"C:\_projects\abc\src\base\cmd\cmdUtils.c"
+"C:\_projects\abc\src\base\io\io.c"
+"C:\_projects\abc\src\base\io\ioReadAiger.c"
+"C:\_projects\abc\src\base\io\ioReadBaf.c"
+"C:\_projects\abc\src\base\io\ioReadBench.c"
+"C:\_projects\abc\src\base\io\ioReadBlif.c"
+"C:\_projects\abc\src\base\io\ioReadBlifAig.c"
+"C:\_projects\abc\src\base\io\ioReadEdif.c"
+"C:\_projects\abc\src\base\io\ioReadEqn.c"
+"C:\_projects\abc\src\base\io\ioReadPla.c"
+"C:\_projects\abc\src\base\io\ioUtil.c"
+"C:\_projects\abc\src\base\io\ioWriteAiger.c"
+"C:\_projects\abc\src\base\io\ioWriteBaf.c"
+"C:\_projects\abc\src\base\io\ioWriteBench.c"
+"C:\_projects\abc\src\base\io\ioWriteBlif.c"
+"C:\_projects\abc\src\base\io\ioWriteCnf.c"
+"C:\_projects\abc\src\base\io\ioWriteDot.c"
+"C:\_projects\abc\src\base\io\ioWriteEqn.c"
+"C:\_projects\abc\src\base\io\ioWriteGml.c"
+"C:\_projects\abc\src\base\io\ioWriteList.c"
+"C:\_projects\abc\src\base\io\ioWritePla.c"
+"C:\_projects\abc\src\base\main\libSupport.c"
+"C:\_projects\abc\src\base\main\main.c"
+"C:\_projects\abc\src\base\main\mainFrame.c"
+"C:\_projects\abc\src\base\main\mainInit.c"
+"C:\_projects\abc\src\base\main\mainUtils.c"
+"C:\_projects\abc\src\base\ver\verCore.c"
+"C:\_projects\abc\src\base\ver\verFormula.c"
+"C:\_projects\abc\src\base\ver\verParse.c"
+"C:\_projects\abc\src\base\ver\verStream.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddAbs.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddApply.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddFind.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddInv.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddIte.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddNeg.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAddWalsh.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAndAbs.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAnneal.c"
+"C:\_projects\abc\src\bdd\cudd\cuddApa.c"
+"C:\_projects\abc\src\bdd\cudd\cuddAPI.c"
+"C:\_projects\abc\src\bdd\cudd\cuddApprox.c"
+"C:\_projects\abc\src\bdd\cudd\cuddBddAbs.c"
+"C:\_projects\abc\src\bdd\cudd\cuddBddCorr.c"
+"C:\_projects\abc\src\bdd\cudd\cuddBddIte.c"
+"C:\_projects\abc\src\bdd\cudd\cuddBridge.c"
+"C:\_projects\abc\src\bdd\cudd\cuddCache.c"
+"C:\_projects\abc\src\bdd\cudd\cuddCheck.c"
+"C:\_projects\abc\src\bdd\cudd\cuddClip.c"
+"C:\_projects\abc\src\bdd\cudd\cuddCof.c"
+"C:\_projects\abc\src\bdd\cudd\cuddCompose.c"
+"C:\_projects\abc\src\bdd\cudd\cuddDecomp.c"
+"C:\_projects\abc\src\bdd\cudd\cuddEssent.c"
+"C:\_projects\abc\src\bdd\cudd\cuddExact.c"
+"C:\_projects\abc\src\bdd\cudd\cuddExport.c"
+"C:\_projects\abc\src\bdd\cudd\cuddGenCof.c"
+"C:\_projects\abc\src\bdd\cudd\cuddGenetic.c"
+"C:\_projects\abc\src\bdd\cudd\cuddGroup.c"
+"C:\_projects\abc\src\bdd\cudd\cuddHarwell.c"
+"C:\_projects\abc\src\bdd\cudd\cuddInit.c"
+"C:\_projects\abc\src\bdd\cudd\cuddInteract.c"
+"C:\_projects\abc\src\bdd\cudd\cuddLCache.c"
+"C:\_projects\abc\src\bdd\cudd\cuddLevelQ.c"
+"C:\_projects\abc\src\bdd\cudd\cuddLinear.c"
+"C:\_projects\abc\src\bdd\cudd\cuddLiteral.c"
+"C:\_projects\abc\src\bdd\cudd\cuddMatMult.c"
+"C:\_projects\abc\src\bdd\cudd\cuddPriority.c"
+"C:\_projects\abc\src\bdd\cudd\cuddRead.c"
+"C:\_projects\abc\src\bdd\cudd\cuddRef.c"
+"C:\_projects\abc\src\bdd\cudd\cuddReorder.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSat.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSign.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSolve.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSplit.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSubsetHB.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSubsetSP.c"
+"C:\_projects\abc\src\bdd\cudd\cuddSymmetry.c"
+"C:\_projects\abc\src\bdd\cudd\cuddTable.c"
+"C:\_projects\abc\src\bdd\cudd\cuddUtil.c"
+"C:\_projects\abc\src\bdd\cudd\cuddWindow.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddCount.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddFuncs.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddGroup.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddIsop.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddLin.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddMisc.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddPort.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddReord.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddSetop.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddSymm.c"
+"C:\_projects\abc\src\bdd\cudd\cuddZddUtil.c"
+"C:\_projects\abc\src\bdd\epd\epd.c"
+"C:\_projects\abc\src\bdd\mtr\mtrBasic.c"
+"C:\_projects\abc\src\bdd\mtr\mtrGroup.c"
+"C:\_projects\abc\src\bdd\parse\parseCore.c"
+"C:\_projects\abc\src\bdd\parse\parseEqn.c"
+"C:\_projects\abc\src\bdd\parse\parseStack.c"
+"C:\_projects\abc\src\bdd\dsd\dsdApi.c"
+"C:\_projects\abc\src\bdd\dsd\dsdCheck.c"
+"C:\_projects\abc\src\bdd\dsd\dsdLocal.c"
+"C:\_projects\abc\src\bdd\dsd\dsdMan.c"
+"C:\_projects\abc\src\bdd\dsd\dsdProc.c"
+"C:\_projects\abc\src\bdd\dsd\dsdTree.c"
+"C:\_projects\abc\src\bdd\reo\reoApi.c"
+"C:\_projects\abc\src\bdd\reo\reoCore.c"
+"C:\_projects\abc\src\bdd\reo\reoProfile.c"
+"C:\_projects\abc\src\bdd\reo\reoSift.c"
+"C:\_projects\abc\src\bdd\reo\reoSwap.c"
+"C:\_projects\abc\src\bdd\reo\reoTest.c"
+"C:\_projects\abc\src\bdd\reo\reoTransfer.c"
+"C:\_projects\abc\src\bdd\reo\reoUnits.c"
+"C:\_projects\abc\src\sat\msat\msatActivity.c"
+"C:\_projects\abc\src\sat\msat\msatClause.c"
+"C:\_projects\abc\src\sat\msat\msatClauseVec.c"
+"C:\_projects\abc\src\sat\msat\msatMem.c"
+"C:\_projects\abc\src\sat\msat\msatOrderH.c"
+"C:\_projects\abc\src\sat\msat\msatQueue.c"
+"C:\_projects\abc\src\sat\msat\msatRead.c"
+"C:\_projects\abc\src\sat\msat\msatSolverApi.c"
+"C:\_projects\abc\src\sat\msat\msatSolverCore.c"
+"C:\_projects\abc\src\sat\msat\msatSolverIo.c"
+"C:\_projects\abc\src\sat\msat\msatSolverSearch.c"
+"C:\_projects\abc\src\sat\msat\msatSort.c"
+"C:\_projects\abc\src\sat\msat\msatVec.c"
+"C:\_projects\abc\src\sat\fraig\fraigApi.c"
+"C:\_projects\abc\src\sat\fraig\fraigCanon.c"
+"C:\_projects\abc\src\sat\fraig\fraigChoice.c"
+"C:\_projects\abc\src\sat\fraig\fraigFanout.c"
+"C:\_projects\abc\src\sat\fraig\fraigFeed.c"
+"C:\_projects\abc\src\sat\fraig\fraigMan.c"
+"C:\_projects\abc\src\sat\fraig\fraigMem.c"
+"C:\_projects\abc\src\sat\fraig\fraigNode.c"
+"C:\_projects\abc\src\sat\fraig\fraigPrime.c"
+"C:\_projects\abc\src\sat\fraig\fraigSat.c"
+"C:\_projects\abc\src\sat\fraig\fraigTable.c"
+"C:\_projects\abc\src\sat\fraig\fraigUtil.c"
+"C:\_projects\abc\src\sat\fraig\fraigVec.c"
+"C:\_projects\abc\src\sat\csat\csat_apis.c"
+"C:\_projects\abc\src\sat\bsat\satMem.c"
+"C:\_projects\abc\src\sat\bsat\satSolver.c"
+"C:\_projects\abc\src\sat\bsat\satUtil.c"
+"C:\_projects\abc\src\opt\fxu\fxu.c"
+"C:\_projects\abc\src\opt\fxu\fxuCreate.c"
+"C:\_projects\abc\src\opt\fxu\fxuHeapD.c"
+"C:\_projects\abc\src\opt\fxu\fxuHeapS.c"
+"C:\_projects\abc\src\opt\fxu\fxuList.c"
+"C:\_projects\abc\src\opt\fxu\fxuMatrix.c"
+"C:\_projects\abc\src\opt\fxu\fxuPair.c"
+"C:\_projects\abc\src\opt\fxu\fxuPrint.c"
+"C:\_projects\abc\src\opt\fxu\fxuReduce.c"
+"C:\_projects\abc\src\opt\fxu\fxuSelect.c"
+"C:\_projects\abc\src\opt\fxu\fxuSingle.c"
+"C:\_projects\abc\src\opt\fxu\fxuUpdate.c"
+"C:\_projects\abc\src\opt\rwr\rwrDec.c"
+"C:\_projects\abc\src\opt\rwr\rwrEva.c"
+"C:\_projects\abc\src\opt\rwr\rwrExp.c"
+"C:\_projects\abc\src\opt\rwr\rwrLib.c"
+"C:\_projects\abc\src\opt\rwr\rwrMan.c"
+"C:\_projects\abc\src\opt\rwr\rwrPrint.c"
+"C:\_projects\abc\src\opt\rwr\rwrTemp.c"
+"C:\_projects\abc\src\opt\rwr\rwrUtil.c"
+"C:\_projects\abc\src\opt\cut\cutApi.c"
+"C:\_projects\abc\src\opt\cut\cutCut.c"
+"C:\_projects\abc\src\opt\cut\cutExpand.c"
+"C:\_projects\abc\src\opt\cut\cutMan.c"
+"C:\_projects\abc\src\opt\cut\cutMerge.c"
+"C:\_projects\abc\src\opt\cut\cutNode.c"
+"C:\_projects\abc\src\opt\cut\cutOracle.c"
+"C:\_projects\abc\src\opt\cut\cutPre22.c"
+"C:\_projects\abc\src\opt\cut\cutSeq.c"
+"C:\_projects\abc\src\opt\cut\cutTruth.c"
+"C:\_projects\abc\src\opt\dec\decAbc.c"
+"C:\_projects\abc\src\opt\dec\decFactor.c"
+"C:\_projects\abc\src\opt\dec\decMan.c"
+"C:\_projects\abc\src\opt\dec\decPrint.c"
+"C:\_projects\abc\src\opt\dec\decUtil.c"
+"C:\_projects\abc\src\opt\sim\simMan.c"
+"C:\_projects\abc\src\opt\sim\simSat.c"
+"C:\_projects\abc\src\opt\sim\simSeq.c"
+"C:\_projects\abc\src\opt\sim\simSupp.c"
+"C:\_projects\abc\src\opt\sim\simSwitch.c"
+"C:\_projects\abc\src\opt\sim\simSym.c"
+"C:\_projects\abc\src\opt\sim\simSymSat.c"
+"C:\_projects\abc\src\opt\sim\simSymSim.c"
+"C:\_projects\abc\src\opt\sim\simSymStr.c"
+"C:\_projects\abc\src\opt\sim\simUtils.c"
+"C:\_projects\abc\src\opt\ret\retArea.c"
+"C:\_projects\abc\src\opt\ret\retCore.c"
+"C:\_projects\abc\src\opt\ret\retDelay.c"
+"C:\_projects\abc\src\opt\ret\retFlow.c"
+"C:\_projects\abc\src\opt\ret\retIncrem.c"
+"C:\_projects\abc\src\opt\ret\retInit.c"
+"C:\_projects\abc\src\opt\ret\retLvalue.c"
+"C:\_projects\abc\src\map\fpga\fpga.c"
+"C:\_projects\abc\src\map\fpga\fpgaCore.c"
+"C:\_projects\abc\src\map\fpga\fpgaCreate.c"
+"C:\_projects\abc\src\map\fpga\fpgaCut.c"
+"C:\_projects\abc\src\map\fpga\fpgaCutUtils.c"
+"C:\_projects\abc\src\map\fpga\fpgaFanout.c"
+"C:\_projects\abc\src\map\fpga\fpgaLib.c"
+"C:\_projects\abc\src\map\fpga\fpgaMatch.c"
+"C:\_projects\abc\src\map\fpga\fpgaSwitch.c"
+"C:\_projects\abc\src\map\fpga\fpgaTime.c"
+"C:\_projects\abc\src\map\fpga\fpgaTruth.c"
+"C:\_projects\abc\src\map\fpga\fpgaUtils.c"
+"C:\_projects\abc\src\map\fpga\fpgaVec.c"
+"C:\_projects\abc\src\map\mapper\mapper.c"
+"C:\_projects\abc\src\map\mapper\mapperCanon.c"
+"C:\_projects\abc\src\map\mapper\mapperCore.c"
+"C:\_projects\abc\src\map\mapper\mapperCreate.c"
+"C:\_projects\abc\src\map\mapper\mapperCut.c"
+"C:\_projects\abc\src\map\mapper\mapperCutUtils.c"
+"C:\_projects\abc\src\map\mapper\mapperFanout.c"
+"C:\_projects\abc\src\map\mapper\mapperLib.c"
+"C:\_projects\abc\src\map\mapper\mapperMatch.c"
+"C:\_projects\abc\src\map\mapper\mapperRefs.c"
+"C:\_projects\abc\src\map\mapper\mapperSuper.c"
+"C:\_projects\abc\src\map\mapper\mapperSwitch.c"
+"C:\_projects\abc\src\map\mapper\mapperTable.c"
+"C:\_projects\abc\src\map\mapper\mapperTime.c"
+"C:\_projects\abc\src\map\mapper\mapperTree.c"
+"C:\_projects\abc\src\map\mapper\mapperTruth.c"
+"C:\_projects\abc\src\map\mapper\mapperUtils.c"
+"C:\_projects\abc\src\map\mapper\mapperVec.c"
+"C:\_projects\abc\src\map\mio\mio.c"
+"C:\_projects\abc\src\map\mio\mioApi.c"
+"C:\_projects\abc\src\map\mio\mioFunc.c"
+"C:\_projects\abc\src\map\mio\mioRead.c"
+"C:\_projects\abc\src\map\mio\mioUtils.c"
+"C:\_projects\abc\src\map\super\super.c"
+"C:\_projects\abc\src\map\super\superAnd.c"
+"C:\_projects\abc\src\map\super\superGate.c"
+"C:\_projects\abc\src\map\super\superWrite.c"
+"C:\_projects\abc\src\map\if\ifCore.c"
+"C:\_projects\abc\src\map\if\ifCut.c"
+"C:\_projects\abc\src\map\if\ifMan.c"
+"C:\_projects\abc\src\map\if\ifMap.c"
+"C:\_projects\abc\src\map\if\ifReduce.c"
+"C:\_projects\abc\src\map\if\ifSeq.c"
+"C:\_projects\abc\src\map\if\ifTime.c"
+"C:\_projects\abc\src\map\if\ifTruth.c"
+"C:\_projects\abc\src\map\if\ifUtil.c"
+"C:\_projects\abc\src\misc\extra\extraBddAuto.c"
+"C:\_projects\abc\src\misc\extra\extraBddKmap.c"
+"C:\_projects\abc\src\misc\extra\extraBddMisc.c"
+"C:\_projects\abc\src\misc\extra\extraBddSymm.c"
+"C:\_projects\abc\src\misc\extra\extraBddUnate.c"
+"C:\_projects\abc\src\misc\extra\extraUtilBitMatrix.c"
+"C:\_projects\abc\src\misc\extra\extraUtilCanon.c"
+"C:\_projects\abc\src\misc\extra\extraUtilFile.c"
+"C:\_projects\abc\src\misc\extra\extraUtilMemory.c"
+"C:\_projects\abc\src\misc\extra\extraUtilMisc.c"
+"C:\_projects\abc\src\misc\extra\extraUtilProgress.c"
+"C:\_projects\abc\src\misc\extra\extraUtilReader.c"
+"C:\_projects\abc\src\misc\extra\extraUtilTruth.c"
+"C:\_projects\abc\src\misc\extra\extraUtilUtil.c"
+"C:\_projects\abc\src\misc\st\st.c"
+"C:\_projects\abc\src\misc\st\stmm.c"
+"C:\_projects\abc\src\misc\mvc\mvc.c"
+"C:\_projects\abc\src\misc\mvc\mvcApi.c"
+"C:\_projects\abc\src\misc\mvc\mvcCompare.c"
+"C:\_projects\abc\src\misc\mvc\mvcContain.c"
+"C:\_projects\abc\src\misc\mvc\mvcCover.c"
+"C:\_projects\abc\src\misc\mvc\mvcCube.c"
+"C:\_projects\abc\src\misc\mvc\mvcDivide.c"
+"C:\_projects\abc\src\misc\mvc\mvcDivisor.c"
+"C:\_projects\abc\src\misc\mvc\mvcList.c"
+"C:\_projects\abc\src\misc\mvc\mvcLits.c"
+"C:\_projects\abc\src\misc\mvc\mvcMan.c"
+"C:\_projects\abc\src\misc\mvc\mvcOpAlg.c"
+"C:\_projects\abc\src\misc\mvc\mvcOpBool.c"
+"C:\_projects\abc\src\misc\mvc\mvcPrint.c"
+"C:\_projects\abc\src\misc\mvc\mvcSort.c"
+"C:\_projects\abc\src\misc\mvc\mvcUtils.c"
+"C:\_projects\abc\src\misc\espresso\cofactor.c"
+"C:\_projects\abc\src\misc\espresso\cols.c"
+"C:\_projects\abc\src\misc\espresso\compl.c"
+"C:\_projects\abc\src\misc\espresso\contain.c"
+"C:\_projects\abc\src\misc\espresso\cubehack.c"
+"C:\_projects\abc\src\misc\espresso\cubestr.c"
+"C:\_projects\abc\src\misc\espresso\cvrin.c"
+"C:\_projects\abc\src\misc\espresso\cvrm.c"
+"C:\_projects\abc\src\misc\espresso\cvrmisc.c"
+"C:\_projects\abc\src\misc\espresso\cvrout.c"
+"C:\_projects\abc\src\misc\espresso\dominate.c"
+"C:\_projects\abc\src\misc\espresso\equiv.c"
+"C:\_projects\abc\src\misc\espresso\espresso.c"
+"C:\_projects\abc\src\misc\espresso\essen.c"
+"C:\_projects\abc\src\misc\espresso\exact.c"
+"C:\_projects\abc\src\misc\espresso\expand.c"
+"C:\_projects\abc\src\misc\espresso\gasp.c"
+"C:\_projects\abc\src\misc\espresso\gimpel.c"
+"C:\_projects\abc\src\misc\espresso\globals.c"
+"C:\_projects\abc\src\misc\espresso\hack.c"
+"C:\_projects\abc\src\misc\espresso\indep.c"
+"C:\_projects\abc\src\misc\espresso\irred.c"
+"C:\_projects\abc\src\misc\espresso\map.c"
+"C:\_projects\abc\src\misc\espresso\matrix.c"
+"C:\_projects\abc\src\misc\espresso\mincov.c"
+"C:\_projects\abc\src\misc\espresso\opo.c"
+"C:\_projects\abc\src\misc\espresso\pair.c"
+"C:\_projects\abc\src\misc\espresso\part.c"
+"C:\_projects\abc\src\misc\espresso\primes.c"
+"C:\_projects\abc\src\misc\espresso\reduce.c"
+"C:\_projects\abc\src\misc\espresso\rows.c"
+"C:\_projects\abc\src\misc\espresso\set.c"
+"C:\_projects\abc\src\misc\espresso\setc.c"
+"C:\_projects\abc\src\misc\espresso\sharp.c"
+"C:\_projects\abc\src\misc\espresso\sminterf.c"
+"C:\_projects\abc\src\misc\espresso\solution.c"
+"C:\_projects\abc\src\misc\espresso\sparse.c"
+"C:\_projects\abc\src\misc\espresso\unate.c"
+"C:\_projects\abc\src\misc\espresso\verify.c"
+"C:\_projects\abc\src\misc\nm\nmApi.c"
+"C:\_projects\abc\src\misc\nm\nmTable.c"
+"C:\_projects\abc\src\aig\hop\hopBalance.c"
+"C:\_projects\abc\src\aig\hop\hopCheck.c"
+"C:\_projects\abc\src\aig\hop\hopDfs.c"
+"C:\_projects\abc\src\aig\hop\hopMan.c"
+"C:\_projects\abc\src\aig\hop\hopMem.c"
+"C:\_projects\abc\src\aig\hop\hopObj.c"
+"C:\_projects\abc\src\aig\hop\hopOper.c"
+"C:\_projects\abc\src\aig\hop\hopTable.c"
+"C:\_projects\abc\src\aig\hop\hopUtil.c"
+"C:\_projects\abc\src\aig\ivy\ivyBalance.c"
+"C:\_projects\abc\src\aig\ivy\ivyCanon.c"
+"C:\_projects\abc\src\aig\ivy\ivyCheck.c"
+"C:\_projects\abc\src\aig\ivy\ivyCut.c"
+"C:\_projects\abc\src\aig\ivy\ivyCutTrav.c"
+"C:\_projects\abc\src\aig\ivy\ivyDfs.c"
+"C:\_projects\abc\src\aig\ivy\ivyDsd.c"
+"C:\_projects\abc\src\aig\ivy\ivyFanout.c"
+"C:\_projects\abc\src\aig\ivy\ivyFastMap.c"
+"C:\_projects\abc\src\aig\ivy\ivyFraig.c"
+"C:\_projects\abc\src\aig\ivy\ivyHaig.c"
+"C:\_projects\abc\src\aig\ivy\ivyMan.c"
+"C:\_projects\abc\src\aig\ivy\ivyMem.c"
+"C:\_projects\abc\src\aig\ivy\ivyMulti.c"
+"C:\_projects\abc\src\aig\ivy\ivyObj.c"
+"C:\_projects\abc\src\aig\ivy\ivyOper.c"
+"C:\_projects\abc\src\aig\ivy\ivyResyn.c"
+"C:\_projects\abc\src\aig\ivy\ivyRwr.c"
+"C:\_projects\abc\src\aig\ivy\ivySeq.c"
+"C:\_projects\abc\src\aig\ivy\ivyShow.c"
+"C:\_projects\abc\src\aig\ivy\ivyTable.c"
+"C:\_projects\abc\src\aig\ivy\ivyUtil.c"
+"C:\_projects\abc\src\aig\rwt\rwtDec.c"
+"C:\_projects\abc\src\aig\rwt\rwtMan.c"
+"C:\_projects\abc\src\aig\rwt\rwtUtil.c"
+"C:\_projects\abc\src\aig\mem\mem.c"
+"C:\_projects\abc\src\base\abc\abcHie.c"
+"C:\_projects\abc\src\base\abc\abcBlifMv.c"
+"C:\_projects\abc\src\base\abci\abcCas.c"
+"C:\_projects\abc\src\base\abci\abcDar.c"
+"C:\_projects\abc\src\base\abci\abcHaig.c"
+"C:\_projects\abc\src\base\abci\abcMeasure.c"
+"C:\_projects\abc\src\base\abci\abcOdc.c"
+"C:\_projects\abc\src\base\abci\abcPart.c"
+"C:\_projects\abc\src\base\abci\abcRec.c"
+"C:\_projects\abc\src\base\abci\abcQbf.c"
+"C:\_projects\abc\src\base\abci\abcQuant.c"
+"C:\_projects\abc\src\base\io\ioReadDsd.c"
+"C:\_projects\abc\src\base\io\ioReadBlifMv.c"
+"C:\_projects\abc\src\base\io\ioReadVerilog.c"
+"C:\_projects\abc\src\base\io\ioWriteVerilog.c"
+"C:\_projects\abc\src\base\io\ioWriteBlifMv.c"
+"C:\_projects\abc\src\bdd\cas\casDec.c"
+"C:\_projects\abc\src\bdd\cas\casCore.c"
+"C:\_projects\abc\src\sat\proof\pr.c"
+"C:\_projects\abc\src\sat\bsat\satTrace.c"
+"C:\_projects\abc\src\sat\bsat\satInter.c"
+"C:\_projects\abc\src\sat\bsat\satStore.c"
+"C:\_projects\abc\src\misc\extra\extraBddCas.c"
+"C:\_projects\abc\src\aig\ioa\ioaWriteAig.c"
+"C:\_projects\abc\src\aig\ioa\ioaReadAig.c"
+"C:\_projects\abc\src\aig\ioa\ioaUtil.c"
+"C:\_projects\abc\src\aig\dar\darBalance.c"
+"C:\_projects\abc\src\aig\dar\darCore.c"
+"C:\_projects\abc\src\aig\dar\darCut.c"
+"C:\_projects\abc\src\aig\dar\darData.c"
+"C:\_projects\abc\src\aig\dar\darLib.c"
+"C:\_projects\abc\src\aig\dar\darMan.c"
+"C:\_projects\abc\src\aig\dar\darPrec.c"
+"C:\_projects\abc\src\aig\dar\darRefact.c"
+"C:\_projects\abc\src\aig\dar\darResub.c"
+"C:\_projects\abc\src\aig\dar\darScript.c"
+"C:\_projects\abc\src\aig\fra\fraBmc.c"
+"C:\_projects\abc\src\aig\fra\fraCec.c"
+"C:\_projects\abc\src\aig\fra\fraClass.c"
+"C:\_projects\abc\src\aig\fra\fraCnf.c"
+"C:\_projects\abc\src\aig\fra\fraCore.c"
+"C:\_projects\abc\src\aig\fra\fraImp.c"
+"C:\_projects\abc\src\aig\fra\fraInd.c"
+"C:\_projects\abc\src\aig\fra\fraLcr.c"
+"C:\_projects\abc\src\aig\fra\fraMan.c"
+"C:\_projects\abc\src\aig\fra\fraPart.c"
+"C:\_projects\abc\src\aig\fra\fraSat.c"
+"C:\_projects\abc\src\aig\fra\fraSec.c"
+"C:\_projects\abc\src\aig\fra\fraSim.c"
+"C:\_projects\abc\src\aig\cnf\cnfCore.c"
+"C:\_projects\abc\src\aig\cnf\cnfCut.c"
+"C:\_projects\abc\src\aig\cnf\cnfData.c"
+"C:\_projects\abc\src\aig\cnf\cnfMan.c"
+"C:\_projects\abc\src\aig\cnf\cnfMap.c"
+"C:\_projects\abc\src\aig\cnf\cnfPost.c"
+"C:\_projects\abc\src\aig\cnf\cnfUtil.c"
+"C:\_projects\abc\src\aig\cnf\cnfWrite.c"
+"C:\_projects\abc\src\aig\csw\cswCore.c"
+"C:\_projects\abc\src\aig\csw\cswCut.c"
+"C:\_projects\abc\src\aig\csw\cswMan.c"
+"C:\_projects\abc\src\aig\csw\cswTable.c"
+"C:\_projects\abc\src\aig\kit\cloud.c"
+"C:\_projects\abc\src\aig\kit\kitAig.c"
+"C:\_projects\abc\src\aig\kit\kitBdd.c"
+"C:\_projects\abc\src\aig\kit\kitCloud.c"
+"C:\_projects\abc\src\aig\kit\kitDsd.c"
+"C:\_projects\abc\src\aig\kit\kitFactor.c"
+"C:\_projects\abc\src\aig\kit\kitGraph.c"
+"C:\_projects\abc\src\aig\kit\kitHop.c"
+"C:\_projects\abc\src\aig\kit\kitIsop.c"
+"C:\_projects\abc\src\aig\kit\kitSop.c"
+"C:\_projects\abc\src\aig\kit\kitTruth.c"
+"C:\_projects\abc\src\aig\bdc\bdcCore.c"
+"C:\_projects\abc\src\aig\bdc\bdcDec.c"
+"C:\_projects\abc\src\aig\bdc\bdcTable.c"
+"C:\_projects\abc\src\aig\aig\aigCheck.c"
+"C:\_projects\abc\src\aig\aig\aigDfs.c"
+"C:\_projects\abc\src\aig\aig\aigFanout.c"
+"C:\_projects\abc\src\aig\aig\aigMan.c"
+"C:\_projects\abc\src\aig\aig\aigMem.c"
+"C:\_projects\abc\src\aig\aig\aigMffc.c"
+"C:\_projects\abc\src\aig\aig\aigObj.c"
+"C:\_projects\abc\src\aig\aig\aigOper.c"
+"C:\_projects\abc\src\aig\aig\aigOrder.c"
+"C:\_projects\abc\src\aig\aig\aigPart.c"
+"C:\_projects\abc\src\aig\aig\aigRepr.c"
+"C:\_projects\abc\src\aig\aig\aigRet.c"
+"C:\_projects\abc\src\aig\aig\aigScl.c"
+"C:\_projects\abc\src\aig\aig\aigSeq.c"
+"C:\_projects\abc\src\aig\aig\aigShow.c"
+"C:\_projects\abc\src\aig\aig\aigTable.c"
+"C:\_projects\abc\src\aig\aig\aigTime.c"
+"C:\_projects\abc\src\aig\aig\aigTiming.c"
+"C:\_projects\abc\src\aig\aig\aigTruth.c"
+"C:\_projects\abc\src\aig\aig\aigTsim.c"
+"C:\_projects\abc\src\aig\aig\aigUtil.c"
+"C:\_projects\abc\src\aig\aig\aigWin.c"
+"C:\_projects\abc\src\aig\bar\bar.c"
+"C:\_projects\abc\src\opt\res\resCore.c"
+"C:\_projects\abc\src\opt\res\resDivs.c"
+"C:\_projects\abc\src\opt\res\resFilter.c"
+"C:\_projects\abc\src\opt\res\resSat.c"
+"C:\_projects\abc\src\opt\res\resSim.c"
+"C:\_projects\abc\src\opt\res\resStrash.c"
+"C:\_projects\abc\src\opt\res\resWin.c"
+"C:\_projects\abc\src\opt\lpk\lpkAbcDec.c"
+"C:\_projects\abc\src\opt\lpk\lpkAbcDsd.c"
+"C:\_projects\abc\src\opt\lpk\lpkAbcMux.c"
+"C:\_projects\abc\src\opt\lpk\lpkAbcUtil.c"
+"C:\_projects\abc\src\opt\lpk\lpkCore.c"
+"C:\_projects\abc\src\opt\lpk\lpkCut.c"
+"C:\_projects\abc\src\opt\lpk\lpkMan.c"
+"C:\_projects\abc\src\opt\lpk\lpkMap.c"
+"C:\_projects\abc\src\opt\lpk\lpkMulti.c"
+"C:\_projects\abc\src\opt\lpk\lpkMux.c"
+"C:\_projects\abc\src\opt\lpk\lpkSets.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AB.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AC.tmp" with contents
+[
+/nologo /out:"abclib\abclib_debug.lib" 
+.\abclib\DebugLib\abcAig.obj
+.\abclib\DebugLib\abcCheck.obj
+.\abclib\DebugLib\abcDfs.obj
+.\abclib\DebugLib\abcFanio.obj
+.\abclib\DebugLib\abcFunc.obj
+.\abclib\DebugLib\abcLatch.obj
+.\abclib\DebugLib\abcLib.obj
+.\abclib\DebugLib\abcMinBase.obj
+.\abclib\DebugLib\abcNames.obj
+.\abclib\DebugLib\abcNetlist.obj
+.\abclib\DebugLib\abcNtk.obj
+.\abclib\DebugLib\abcObj.obj
+.\abclib\DebugLib\abcRefs.obj
+.\abclib\DebugLib\abcShow.obj
+.\abclib\DebugLib\abcSop.obj
+.\abclib\DebugLib\abcUtil.obj
+.\abclib\DebugLib\abc.obj
+.\abclib\DebugLib\abcAttach.obj
+.\abclib\DebugLib\abcAuto.obj
+.\abclib\DebugLib\abcBalance.obj
+.\abclib\DebugLib\abcBmc.obj
+.\abclib\DebugLib\abcClpBdd.obj
+.\abclib\DebugLib\abcClpSop.obj
+.\abclib\DebugLib\abcCut.obj
+.\abclib\DebugLib\abcDebug.obj
+.\abclib\DebugLib\abcDress.obj
+.\abclib\DebugLib\abcDsd.obj
+.\abclib\DebugLib\abcEspresso.obj
+.\abclib\DebugLib\abcExtract.obj
+.\abclib\DebugLib\abcFpga.obj
+.\abclib\DebugLib\abcFpgaFast.obj
+.\abclib\DebugLib\abcFraig.obj
+.\abclib\DebugLib\abcFxu.obj
+.\abclib\DebugLib\abcGen.obj
+.\abclib\DebugLib\abcIf.obj
+.\abclib\DebugLib\abcIvy.obj
+.\abclib\DebugLib\abcLut.obj
+.\abclib\DebugLib\abcMap.obj
+.\abclib\DebugLib\abcMini.obj
+.\abclib\DebugLib\abcMiter.obj
+.\abclib\DebugLib\abcMulti.obj
+.\abclib\DebugLib\abcMv.obj
+.\abclib\DebugLib\abcNtbdd.obj
+.\abclib\DebugLib\abcOrder.obj
+.\abclib\DebugLib\abcPrint.obj
+.\abclib\DebugLib\abcProve.obj
+.\abclib\DebugLib\abcReconv.obj
+.\abclib\DebugLib\abcRefactor.obj
+.\abclib\DebugLib\abcRenode.obj
+.\abclib\DebugLib\abcReorder.obj
+.\abclib\DebugLib\abcRestruct.obj
+.\abclib\DebugLib\abcResub.obj
+.\abclib\DebugLib\abcRewrite.obj
+.\abclib\DebugLib\abcRr.obj
+.\abclib\DebugLib\abcSat.obj
+.\abclib\DebugLib\abcStrash.obj
+.\abclib\DebugLib\abcSweep.obj
+.\abclib\DebugLib\abcSymm.obj
+.\abclib\DebugLib\abcTiming.obj
+.\abclib\DebugLib\abcUnate.obj
+.\abclib\DebugLib\abcUnreach.obj
+.\abclib\DebugLib\abcVerify.obj
+.\abclib\DebugLib\abcXsim.obj
+.\abclib\DebugLib\cmd.obj
+.\abclib\DebugLib\cmdAlias.obj
+.\abclib\DebugLib\cmdApi.obj
+.\abclib\DebugLib\cmdFlag.obj
+.\abclib\DebugLib\cmdHist.obj
+.\abclib\DebugLib\cmdUtils.obj
+.\abclib\DebugLib\io.obj
+.\abclib\DebugLib\ioReadAiger.obj
+.\abclib\DebugLib\ioReadBaf.obj
+.\abclib\DebugLib\ioReadBench.obj
+.\abclib\DebugLib\ioReadBlif.obj
+.\abclib\DebugLib\ioReadBlifAig.obj
+.\abclib\DebugLib\ioReadEdif.obj
+.\abclib\DebugLib\ioReadEqn.obj
+.\abclib\DebugLib\ioReadPla.obj
+.\abclib\DebugLib\ioUtil.obj
+.\abclib\DebugLib\ioWriteAiger.obj
+.\abclib\DebugLib\ioWriteBaf.obj
+.\abclib\DebugLib\ioWriteBench.obj
+.\abclib\DebugLib\ioWriteBlif.obj
+.\abclib\DebugLib\ioWriteCnf.obj
+.\abclib\DebugLib\ioWriteDot.obj
+.\abclib\DebugLib\ioWriteEqn.obj
+.\abclib\DebugLib\ioWriteGml.obj
+.\abclib\DebugLib\ioWriteList.obj
+.\abclib\DebugLib\ioWritePla.obj
+.\abclib\DebugLib\libSupport.obj
+.\abclib\DebugLib\main.obj
+.\abclib\DebugLib\mainFrame.obj
+.\abclib\DebugLib\mainInit.obj
+.\abclib\DebugLib\mainUtils.obj
+.\abclib\DebugLib\verCore.obj
+.\abclib\DebugLib\verFormula.obj
+.\abclib\DebugLib\verParse.obj
+.\abclib\DebugLib\verStream.obj
+.\abclib\DebugLib\cuddAddAbs.obj
+.\abclib\DebugLib\cuddAddApply.obj
+.\abclib\DebugLib\cuddAddFind.obj
+.\abclib\DebugLib\cuddAddInv.obj
+.\abclib\DebugLib\cuddAddIte.obj
+.\abclib\DebugLib\cuddAddNeg.obj
+.\abclib\DebugLib\cuddAddWalsh.obj
+.\abclib\DebugLib\cuddAndAbs.obj
+.\abclib\DebugLib\cuddAnneal.obj
+.\abclib\DebugLib\cuddApa.obj
+.\abclib\DebugLib\cuddAPI.obj
+.\abclib\DebugLib\cuddApprox.obj
+.\abclib\DebugLib\cuddBddAbs.obj
+.\abclib\DebugLib\cuddBddCorr.obj
+.\abclib\DebugLib\cuddBddIte.obj
+.\abclib\DebugLib\cuddBridge.obj
+.\abclib\DebugLib\cuddCache.obj
+.\abclib\DebugLib\cuddCheck.obj
+.\abclib\DebugLib\cuddClip.obj
+.\abclib\DebugLib\cuddCof.obj
+.\abclib\DebugLib\cuddCompose.obj
+.\abclib\DebugLib\cuddDecomp.obj
+.\abclib\DebugLib\cuddEssent.obj
+.\abclib\DebugLib\cuddExact.obj
+.\abclib\DebugLib\cuddExport.obj
+.\abclib\DebugLib\cuddGenCof.obj
+.\abclib\DebugLib\cuddGenetic.obj
+.\abclib\DebugLib\cuddGroup.obj
+.\abclib\DebugLib\cuddHarwell.obj
+.\abclib\DebugLib\cuddInit.obj
+.\abclib\DebugLib\cuddInteract.obj
+.\abclib\DebugLib\cuddLCache.obj
+.\abclib\DebugLib\cuddLevelQ.obj
+.\abclib\DebugLib\cuddLinear.obj
+.\abclib\DebugLib\cuddLiteral.obj
+.\abclib\DebugLib\cuddMatMult.obj
+.\abclib\DebugLib\cuddPriority.obj
+.\abclib\DebugLib\cuddRead.obj
+.\abclib\DebugLib\cuddRef.obj
+.\abclib\DebugLib\cuddReorder.obj
+.\abclib\DebugLib\cuddSat.obj
+.\abclib\DebugLib\cuddSign.obj
+.\abclib\DebugLib\cuddSolve.obj
+.\abclib\DebugLib\cuddSplit.obj
+.\abclib\DebugLib\cuddSubsetHB.obj
+.\abclib\DebugLib\cuddSubsetSP.obj
+.\abclib\DebugLib\cuddSymmetry.obj
+.\abclib\DebugLib\cuddTable.obj
+.\abclib\DebugLib\cuddUtil.obj
+.\abclib\DebugLib\cuddWindow.obj
+.\abclib\DebugLib\cuddZddCount.obj
+.\abclib\DebugLib\cuddZddFuncs.obj
+.\abclib\DebugLib\cuddZddGroup.obj
+.\abclib\DebugLib\cuddZddIsop.obj
+.\abclib\DebugLib\cuddZddLin.obj
+.\abclib\DebugLib\cuddZddMisc.obj
+.\abclib\DebugLib\cuddZddPort.obj
+.\abclib\DebugLib\cuddZddReord.obj
+.\abclib\DebugLib\cuddZddSetop.obj
+.\abclib\DebugLib\cuddZddSymm.obj
+.\abclib\DebugLib\cuddZddUtil.obj
+.\abclib\DebugLib\epd.obj
+.\abclib\DebugLib\mtrBasic.obj
+.\abclib\DebugLib\mtrGroup.obj
+.\abclib\DebugLib\parseCore.obj
+.\abclib\DebugLib\parseEqn.obj
+.\abclib\DebugLib\parseStack.obj
+.\abclib\DebugLib\dsdApi.obj
+.\abclib\DebugLib\dsdCheck.obj
+.\abclib\DebugLib\dsdLocal.obj
+.\abclib\DebugLib\dsdMan.obj
+.\abclib\DebugLib\dsdProc.obj
+.\abclib\DebugLib\dsdTree.obj
+.\abclib\DebugLib\reoApi.obj
+.\abclib\DebugLib\reoCore.obj
+.\abclib\DebugLib\reoProfile.obj
+.\abclib\DebugLib\reoSift.obj
+.\abclib\DebugLib\reoSwap.obj
+.\abclib\DebugLib\reoTest.obj
+.\abclib\DebugLib\reoTransfer.obj
+.\abclib\DebugLib\reoUnits.obj
+.\abclib\DebugLib\msatActivity.obj
+.\abclib\DebugLib\msatClause.obj
+.\abclib\DebugLib\msatClauseVec.obj
+.\abclib\DebugLib\msatMem.obj
+.\abclib\DebugLib\msatOrderH.obj
+.\abclib\DebugLib\msatQueue.obj
+.\abclib\DebugLib\msatRead.obj
+.\abclib\DebugLib\msatSolverApi.obj
+.\abclib\DebugLib\msatSolverCore.obj
+.\abclib\DebugLib\msatSolverIo.obj
+.\abclib\DebugLib\msatSolverSearch.obj
+.\abclib\DebugLib\msatSort.obj
+.\abclib\DebugLib\msatVec.obj
+.\abclib\DebugLib\fraigApi.obj
+.\abclib\DebugLib\fraigCanon.obj
+.\abclib\DebugLib\fraigChoice.obj
+.\abclib\DebugLib\fraigFanout.obj
+.\abclib\DebugLib\fraigFeed.obj
+.\abclib\DebugLib\fraigMan.obj
+.\abclib\DebugLib\fraigMem.obj
+.\abclib\DebugLib\fraigNode.obj
+.\abclib\DebugLib\fraigPrime.obj
+.\abclib\DebugLib\fraigSat.obj
+.\abclib\DebugLib\fraigTable.obj
+.\abclib\DebugLib\fraigUtil.obj
+.\abclib\DebugLib\fraigVec.obj
+.\abclib\DebugLib\csat_apis.obj
+.\abclib\DebugLib\satMem.obj
+.\abclib\DebugLib\satSolver.obj
+.\abclib\DebugLib\satUtil.obj
+.\abclib\DebugLib\fxu.obj
+.\abclib\DebugLib\fxuCreate.obj
+.\abclib\DebugLib\fxuHeapD.obj
+.\abclib\DebugLib\fxuHeapS.obj
+.\abclib\DebugLib\fxuList.obj
+.\abclib\DebugLib\fxuMatrix.obj
+.\abclib\DebugLib\fxuPair.obj
+.\abclib\DebugLib\fxuPrint.obj
+.\abclib\DebugLib\fxuReduce.obj
+.\abclib\DebugLib\fxuSelect.obj
+.\abclib\DebugLib\fxuSingle.obj
+.\abclib\DebugLib\fxuUpdate.obj
+.\abclib\DebugLib\rwrDec.obj
+.\abclib\DebugLib\rwrEva.obj
+.\abclib\DebugLib\rwrExp.obj
+.\abclib\DebugLib\rwrLib.obj
+.\abclib\DebugLib\rwrMan.obj
+.\abclib\DebugLib\rwrPrint.obj
+.\abclib\DebugLib\rwrTemp.obj
+.\abclib\DebugLib\rwrUtil.obj
+.\abclib\DebugLib\cutApi.obj
+.\abclib\DebugLib\cutCut.obj
+.\abclib\DebugLib\cutExpand.obj
+.\abclib\DebugLib\cutMan.obj
+.\abclib\DebugLib\cutMerge.obj
+.\abclib\DebugLib\cutNode.obj
+.\abclib\DebugLib\cutOracle.obj
+.\abclib\DebugLib\cutPre22.obj
+.\abclib\DebugLib\cutSeq.obj
+.\abclib\DebugLib\cutTruth.obj
+.\abclib\DebugLib\decAbc.obj
+.\abclib\DebugLib\decFactor.obj
+.\abclib\DebugLib\decMan.obj
+.\abclib\DebugLib\decPrint.obj
+.\abclib\DebugLib\decUtil.obj
+.\abclib\DebugLib\simMan.obj
+.\abclib\DebugLib\simSat.obj
+.\abclib\DebugLib\simSeq.obj
+.\abclib\DebugLib\simSupp.obj
+.\abclib\DebugLib\simSwitch.obj
+.\abclib\DebugLib\simSym.obj
+.\abclib\DebugLib\simSymSat.obj
+.\abclib\DebugLib\simSymSim.obj
+.\abclib\DebugLib\simSymStr.obj
+.\abclib\DebugLib\simUtils.obj
+.\abclib\DebugLib\retArea.obj
+.\abclib\DebugLib\retCore.obj
+.\abclib\DebugLib\retDelay.obj
+.\abclib\DebugLib\retFlow.obj
+.\abclib\DebugLib\retIncrem.obj
+.\abclib\DebugLib\retInit.obj
+.\abclib\DebugLib\retLvalue.obj
+.\abclib\DebugLib\fpga.obj
+.\abclib\DebugLib\fpgaCore.obj
+.\abclib\DebugLib\fpgaCreate.obj
+.\abclib\DebugLib\fpgaCut.obj
+.\abclib\DebugLib\fpgaCutUtils.obj
+.\abclib\DebugLib\fpgaFanout.obj
+.\abclib\DebugLib\fpgaLib.obj
+.\abclib\DebugLib\fpgaMatch.obj
+.\abclib\DebugLib\fpgaSwitch.obj
+.\abclib\DebugLib\fpgaTime.obj
+.\abclib\DebugLib\fpgaTruth.obj
+.\abclib\DebugLib\fpgaUtils.obj
+.\abclib\DebugLib\fpgaVec.obj
+.\abclib\DebugLib\mapper.obj
+.\abclib\DebugLib\mapperCanon.obj
+.\abclib\DebugLib\mapperCore.obj
+.\abclib\DebugLib\mapperCreate.obj
+.\abclib\DebugLib\mapperCut.obj
+.\abclib\DebugLib\mapperCutUtils.obj
+.\abclib\DebugLib\mapperFanout.obj
+.\abclib\DebugLib\mapperLib.obj
+.\abclib\DebugLib\mapperMatch.obj
+.\abclib\DebugLib\mapperRefs.obj
+.\abclib\DebugLib\mapperSuper.obj
+.\abclib\DebugLib\mapperSwitch.obj
+.\abclib\DebugLib\mapperTable.obj
+.\abclib\DebugLib\mapperTime.obj
+.\abclib\DebugLib\mapperTree.obj
+.\abclib\DebugLib\mapperTruth.obj
+.\abclib\DebugLib\mapperUtils.obj
+.\abclib\DebugLib\mapperVec.obj
+.\abclib\DebugLib\mio.obj
+.\abclib\DebugLib\mioApi.obj
+.\abclib\DebugLib\mioFunc.obj
+.\abclib\DebugLib\mioRead.obj
+.\abclib\DebugLib\mioUtils.obj
+.\abclib\DebugLib\super.obj
+.\abclib\DebugLib\superAnd.obj
+.\abclib\DebugLib\superGate.obj
+.\abclib\DebugLib\superWrite.obj
+.\abclib\DebugLib\ifCore.obj
+.\abclib\DebugLib\ifCut.obj
+.\abclib\DebugLib\ifMan.obj
+.\abclib\DebugLib\ifMap.obj
+.\abclib\DebugLib\ifReduce.obj
+.\abclib\DebugLib\ifSeq.obj
+.\abclib\DebugLib\ifTime.obj
+.\abclib\DebugLib\ifTruth.obj
+.\abclib\DebugLib\ifUtil.obj
+.\abclib\DebugLib\extraBddAuto.obj
+.\abclib\DebugLib\extraBddKmap.obj
+.\abclib\DebugLib\extraBddMisc.obj
+.\abclib\DebugLib\extraBddSymm.obj
+.\abclib\DebugLib\extraBddUnate.obj
+.\abclib\DebugLib\extraUtilBitMatrix.obj
+.\abclib\DebugLib\extraUtilCanon.obj
+.\abclib\DebugLib\extraUtilFile.obj
+.\abclib\DebugLib\extraUtilMemory.obj
+.\abclib\DebugLib\extraUtilMisc.obj
+.\abclib\DebugLib\extraUtilProgress.obj
+.\abclib\DebugLib\extraUtilReader.obj
+.\abclib\DebugLib\extraUtilTruth.obj
+.\abclib\DebugLib\extraUtilUtil.obj
+.\abclib\DebugLib\st.obj
+.\abclib\DebugLib\stmm.obj
+.\abclib\DebugLib\mvc.obj
+.\abclib\DebugLib\mvcApi.obj
+.\abclib\DebugLib\mvcCompare.obj
+.\abclib\DebugLib\mvcContain.obj
+.\abclib\DebugLib\mvcCover.obj
+.\abclib\DebugLib\mvcCube.obj
+.\abclib\DebugLib\mvcDivide.obj
+.\abclib\DebugLib\mvcDivisor.obj
+.\abclib\DebugLib\mvcList.obj
+.\abclib\DebugLib\mvcLits.obj
+.\abclib\DebugLib\mvcMan.obj
+.\abclib\DebugLib\mvcOpAlg.obj
+.\abclib\DebugLib\mvcOpBool.obj
+.\abclib\DebugLib\mvcPrint.obj
+.\abclib\DebugLib\mvcSort.obj
+.\abclib\DebugLib\mvcUtils.obj
+.\abclib\DebugLib\cofactor.obj
+.\abclib\DebugLib\cols.obj
+.\abclib\DebugLib\compl.obj
+.\abclib\DebugLib\contain.obj
+.\abclib\DebugLib\cubehack.obj
+.\abclib\DebugLib\cubestr.obj
+.\abclib\DebugLib\cvrin.obj
+.\abclib\DebugLib\cvrm.obj
+.\abclib\DebugLib\cvrmisc.obj
+.\abclib\DebugLib\cvrout.obj
+.\abclib\DebugLib\dominate.obj
+.\abclib\DebugLib\equiv.obj
+.\abclib\DebugLib\espresso.obj
+.\abclib\DebugLib\essen.obj
+.\abclib\DebugLib\exact.obj
+.\abclib\DebugLib\expand.obj
+.\abclib\DebugLib\gasp.obj
+.\abclib\DebugLib\gimpel.obj
+.\abclib\DebugLib\globals.obj
+.\abclib\DebugLib\hack.obj
+.\abclib\DebugLib\indep.obj
+.\abclib\DebugLib\irred.obj
+.\abclib\DebugLib\map.obj
+.\abclib\DebugLib\matrix.obj
+.\abclib\DebugLib\mincov.obj
+.\abclib\DebugLib\opo.obj
+.\abclib\DebugLib\pair.obj
+.\abclib\DebugLib\part.obj
+.\abclib\DebugLib\primes.obj
+.\abclib\DebugLib\reduce.obj
+.\abclib\DebugLib\rows.obj
+.\abclib\DebugLib\set.obj
+.\abclib\DebugLib\setc.obj
+.\abclib\DebugLib\sharp.obj
+.\abclib\DebugLib\sminterf.obj
+.\abclib\DebugLib\solution.obj
+.\abclib\DebugLib\sparse.obj
+.\abclib\DebugLib\unate.obj
+.\abclib\DebugLib\verify.obj
+.\abclib\DebugLib\nmApi.obj
+.\abclib\DebugLib\nmTable.obj
+.\abclib\DebugLib\hopBalance.obj
+.\abclib\DebugLib\hopCheck.obj
+.\abclib\DebugLib\hopDfs.obj
+.\abclib\DebugLib\hopMan.obj
+.\abclib\DebugLib\hopMem.obj
+.\abclib\DebugLib\hopObj.obj
+.\abclib\DebugLib\hopOper.obj
+.\abclib\DebugLib\hopTable.obj
+.\abclib\DebugLib\hopUtil.obj
+.\abclib\DebugLib\ivyBalance.obj
+.\abclib\DebugLib\ivyCanon.obj
+.\abclib\DebugLib\ivyCheck.obj
+.\abclib\DebugLib\ivyCut.obj
+.\abclib\DebugLib\ivyCutTrav.obj
+.\abclib\DebugLib\ivyDfs.obj
+.\abclib\DebugLib\ivyDsd.obj
+.\abclib\DebugLib\ivyFanout.obj
+.\abclib\DebugLib\ivyFastMap.obj
+.\abclib\DebugLib\ivyFraig.obj
+.\abclib\DebugLib\ivyHaig.obj
+.\abclib\DebugLib\ivyMan.obj
+.\abclib\DebugLib\ivyMem.obj
+.\abclib\DebugLib\ivyMulti.obj
+.\abclib\DebugLib\ivyObj.obj
+.\abclib\DebugLib\ivyOper.obj
+.\abclib\DebugLib\ivyResyn.obj
+.\abclib\DebugLib\ivyRwr.obj
+.\abclib\DebugLib\ivySeq.obj
+.\abclib\DebugLib\ivyShow.obj
+.\abclib\DebugLib\ivyTable.obj
+.\abclib\DebugLib\ivyUtil.obj
+.\abclib\DebugLib\rwtDec.obj
+.\abclib\DebugLib\rwtMan.obj
+.\abclib\DebugLib\rwtUtil.obj
+.\abclib\DebugLib\mem.obj
+.\abclib\DebugLib\abcHie.obj
+.\abclib\DebugLib\abcBlifMv.obj
+.\abclib\DebugLib\abcCas.obj
+.\abclib\DebugLib\abcDar.obj
+.\abclib\DebugLib\abcHaig.obj
+.\abclib\DebugLib\abcMeasure.obj
+.\abclib\DebugLib\abcOdc.obj
+.\abclib\DebugLib\abcPart.obj
+.\abclib\DebugLib\abcRec.obj
+.\abclib\DebugLib\abcQbf.obj
+.\abclib\DebugLib\abcQuant.obj
+.\abclib\DebugLib\ioReadDsd.obj
+.\abclib\DebugLib\ioReadBlifMv.obj
+.\abclib\DebugLib\ioReadVerilog.obj
+.\abclib\DebugLib\ioWriteVerilog.obj
+.\abclib\DebugLib\ioWriteBlifMv.obj
+.\abclib\DebugLib\casDec.obj
+.\abclib\DebugLib\casCore.obj
+.\abclib\DebugLib\pr.obj
+.\abclib\DebugLib\satTrace.obj
+.\abclib\DebugLib\satInter.obj
+.\abclib\DebugLib\satStore.obj
+.\abclib\DebugLib\extraBddCas.obj
+.\abclib\DebugLib\ioaWriteAig.obj
+.\abclib\DebugLib\ioaReadAig.obj
+.\abclib\DebugLib\ioaUtil.obj
+.\abclib\DebugLib\darBalance.obj
+.\abclib\DebugLib\darCore.obj
+.\abclib\DebugLib\darCut.obj
+.\abclib\DebugLib\darData.obj
+.\abclib\DebugLib\darLib.obj
+.\abclib\DebugLib\darMan.obj
+.\abclib\DebugLib\darPrec.obj
+.\abclib\DebugLib\darRefact.obj
+.\abclib\DebugLib\darResub.obj
+.\abclib\DebugLib\darScript.obj
+.\abclib\DebugLib\fraBmc.obj
+.\abclib\DebugLib\fraCec.obj
+.\abclib\DebugLib\fraClass.obj
+.\abclib\DebugLib\fraCnf.obj
+.\abclib\DebugLib\fraCore.obj
+.\abclib\DebugLib\fraImp.obj
+.\abclib\DebugLib\fraInd.obj
+.\abclib\DebugLib\fraLcr.obj
+.\abclib\DebugLib\fraMan.obj
+.\abclib\DebugLib\fraPart.obj
+.\abclib\DebugLib\fraSat.obj
+.\abclib\DebugLib\fraSec.obj
+.\abclib\DebugLib\fraSim.obj
+.\abclib\DebugLib\cnfCore.obj
+.\abclib\DebugLib\cnfCut.obj
+.\abclib\DebugLib\cnfData.obj
+.\abclib\DebugLib\cnfMan.obj
+.\abclib\DebugLib\cnfMap.obj
+.\abclib\DebugLib\cnfPost.obj
+.\abclib\DebugLib\cnfUtil.obj
+.\abclib\DebugLib\cnfWrite.obj
+.\abclib\DebugLib\cswCore.obj
+.\abclib\DebugLib\cswCut.obj
+.\abclib\DebugLib\cswMan.obj
+.\abclib\DebugLib\cswTable.obj
+.\abclib\DebugLib\cloud.obj
+.\abclib\DebugLib\kitAig.obj
+.\abclib\DebugLib\kitBdd.obj
+.\abclib\DebugLib\kitCloud.obj
+.\abclib\DebugLib\kitDsd.obj
+.\abclib\DebugLib\kitFactor.obj
+.\abclib\DebugLib\kitGraph.obj
+.\abclib\DebugLib\kitHop.obj
+.\abclib\DebugLib\kitIsop.obj
+.\abclib\DebugLib\kitSop.obj
+.\abclib\DebugLib\kitTruth.obj
+.\abclib\DebugLib\bdcCore.obj
+.\abclib\DebugLib\bdcDec.obj
+.\abclib\DebugLib\bdcTable.obj
+.\abclib\DebugLib\aigCheck.obj
+.\abclib\DebugLib\aigDfs.obj
+.\abclib\DebugLib\aigFanout.obj
+.\abclib\DebugLib\aigMan.obj
+.\abclib\DebugLib\aigMem.obj
+.\abclib\DebugLib\aigMffc.obj
+.\abclib\DebugLib\aigObj.obj
+.\abclib\DebugLib\aigOper.obj
+.\abclib\DebugLib\aigOrder.obj
+.\abclib\DebugLib\aigPart.obj
+.\abclib\DebugLib\aigRepr.obj
+.\abclib\DebugLib\aigRet.obj
+.\abclib\DebugLib\aigScl.obj
+.\abclib\DebugLib\aigSeq.obj
+.\abclib\DebugLib\aigShow.obj
+.\abclib\DebugLib\aigTable.obj
+.\abclib\DebugLib\aigTime.obj
+.\abclib\DebugLib\aigTiming.obj
+.\abclib\DebugLib\aigTruth.obj
+.\abclib\DebugLib\aigTsim.obj
+.\abclib\DebugLib\aigUtil.obj
+.\abclib\DebugLib\aigWin.obj
+.\abclib\DebugLib\bar.obj
+.\abclib\DebugLib\resCore.obj
+.\abclib\DebugLib\resDivs.obj
+.\abclib\DebugLib\resFilter.obj
+.\abclib\DebugLib\resSat.obj
+.\abclib\DebugLib\resSim.obj
+.\abclib\DebugLib\resStrash.obj
+.\abclib\DebugLib\resWin.obj
+.\abclib\DebugLib\lpkAbcDec.obj
+.\abclib\DebugLib\lpkAbcDsd.obj
+.\abclib\DebugLib\lpkAbcMux.obj
+.\abclib\DebugLib\lpkAbcUtil.obj
+.\abclib\DebugLib\lpkCore.obj
+.\abclib\DebugLib\lpkCut.obj
+.\abclib\DebugLib\lpkMan.obj
+.\abclib\DebugLib\lpkMap.obj
+.\abclib\DebugLib\lpkMulti.obj
+.\abclib\DebugLib\lpkMux.obj
+.\abclib\DebugLib\lpkSets.obj
+]
+Creating command line "link.exe -lib @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AC.tmp"
+<h3>Output Window</h3>
+Compiling...
+abcAig.c
+abcCheck.c
+abcDfs.c
+abcFanio.c
+abcFunc.c
+abcLatch.c
+abcLib.c
+abcMinBase.c
+abcNames.c
+abcNetlist.c
+abcNtk.c
+abcObj.c
+abcRefs.c
+abcShow.c
+abcSop.c
+abcUtil.c
+abc.c
+abcAttach.c
+abcAuto.c
+abcBalance.c
+abcBmc.c
+abcClpBdd.c
+abcClpSop.c
+abcCut.c
+abcDebug.c
+abcDress.c
+abcDsd.c
+abcEspresso.c
+abcExtract.c
+abcFpga.c
+abcFpgaFast.c
+abcFraig.c
+abcFxu.c
+abcGen.c
+abcIf.c
+abcIvy.c
+abcLut.c
+abcMap.c
+abcMini.c
+abcMiter.c
+abcMulti.c
+abcMv.c
+abcNtbdd.c
+abcOrder.c
+abcPrint.c
+abcProve.c
+abcReconv.c
+abcRefactor.c
+abcRenode.c
+abcReorder.c
+abcRestruct.c
+abcResub.c
+abcRewrite.c
+abcRr.c
+abcSat.c
+abcStrash.c
+abcSweep.c
+abcSymm.c
+abcTiming.c
+abcUnate.c
+abcUnreach.c
+abcVerify.c
+abcXsim.c
+cmd.c
+cmdAlias.c
+cmdApi.c
+cmdFlag.c
+cmdHist.c
+cmdUtils.c
+io.c
+ioReadAiger.c
+ioReadBaf.c
+ioReadBench.c
+ioReadBlif.c
+ioReadBlifAig.c
+ioReadEdif.c
+ioReadEqn.c
+ioReadPla.c
+ioUtil.c
+ioWriteAiger.c
+ioWriteBaf.c
+ioWriteBench.c
+ioWriteBlif.c
+ioWriteCnf.c
+ioWriteDot.c
+ioWriteEqn.c
+ioWriteGml.c
+ioWriteList.c
+ioWritePla.c
+libSupport.c
+main.c
+mainFrame.c
+mainInit.c
+mainUtils.c
+verCore.c
+verFormula.c
+verParse.c
+verStream.c
+cuddAddAbs.c
+cuddAddApply.c
+cuddAddFind.c
+cuddAddInv.c
+cuddAddIte.c
+cuddAddNeg.c
+cuddAddWalsh.c
+cuddAndAbs.c
+cuddAnneal.c
+cuddApa.c
+C:\_projects\abc\src\bdd\cudd\cuddApa.c(181) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
+C:\_projects\abc\src\bdd\cudd\cuddApa.c(213) : warning C4244: 'return' : conversion from 'unsigned long ' to 'unsigned short ', possible loss of data
+C:\_projects\abc\src\bdd\cudd\cuddApa.c(530) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
+C:\_projects\abc\src\bdd\cudd\cuddApa.c(588) : warning C4244: '=' : conversion from 'unsigned short ' to 'unsigned char ', possible loss of data
+cuddAPI.c
+cuddApprox.c
+cuddBddAbs.c
+cuddBddCorr.c
+cuddBddIte.c
+cuddBridge.c
+cuddCache.c
+C:\_projects\abc\src\bdd\cudd\cuddCache.c(902) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
+cuddCheck.c
+cuddClip.c
+cuddCof.c
+cuddCompose.c
+cuddDecomp.c
+cuddEssent.c
+cuddExact.c
+cuddExport.c
+cuddGenCof.c
+cuddGenetic.c
+cuddGroup.c
+C:\_projects\abc\src\bdd\cudd\cuddGroup.c(2062) : warning C4018: '<=' : signed/unsigned mismatch
+cuddHarwell.c
+cuddInit.c
+cuddInteract.c
+cuddLCache.c
+c:\_projects\abc\src\bdd\cudd\cuddlcache.c(1387) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
+cuddLevelQ.c
+cuddLinear.c
+cuddLiteral.c
+cuddMatMult.c
+cuddPriority.c
+cuddRead.c
+cuddRef.c
+cuddReorder.c
+C:\_projects\abc\src\bdd\cudd\cuddReorder.c(395) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
+cuddSat.c
+cuddSign.c
+cuddSolve.c
+cuddSplit.c
+cuddSubsetHB.c
+cuddSubsetSP.c
+cuddSymmetry.c
+cuddTable.c
+C:\_projects\abc\src\bdd\cudd\cuddTable.c(1822) : warning C4018: '<' : signed/unsigned mismatch
+C:\_projects\abc\src\bdd\cudd\cuddTable.c(1927) : warning C4018: '<' : signed/unsigned mismatch
+C:\_projects\abc\src\bdd\cudd\cuddTable.c(2235) : warning C4018: '<' : signed/unsigned mismatch
+C:\_projects\abc\src\bdd\cudd\cuddTable.c(2303) : warning C4018: '<' : signed/unsigned mismatch
+C:\_projects\abc\src\bdd\cudd\cuddTable.c(2358) : warning C4146: unary minus operator applied to unsigned type, result still unsigned
+cuddUtil.c
+cuddWindow.c
+cuddZddCount.c
+cuddZddFuncs.c
+cuddZddGroup.c
+cuddZddIsop.c
+cuddZddLin.c
+cuddZddMisc.c
+cuddZddPort.c
+cuddZddReord.c
+cuddZddSetop.c
+cuddZddSymm.c
+cuddZddUtil.c
+epd.c
+mtrBasic.c
+mtrGroup.c
+parseCore.c
+parseEqn.c
+parseStack.c
+dsdApi.c
+dsdCheck.c
+dsdLocal.c
+dsdMan.c
+dsdProc.c
+dsdTree.c
+reoApi.c
+reoCore.c
+reoProfile.c
+reoSift.c
+reoSwap.c
+reoTest.c
+reoTransfer.c
+reoUnits.c
+msatActivity.c
+msatClause.c
+msatClauseVec.c
+msatMem.c
+msatOrderH.c
+msatQueue.c
+msatRead.c
+msatSolverApi.c
+msatSolverCore.c
+msatSolverIo.c
+msatSolverSearch.c
+msatSort.c
+msatVec.c
+fraigApi.c
+fraigCanon.c
+fraigChoice.c
+fraigFanout.c
+fraigFeed.c
+fraigMan.c
+fraigMem.c
+fraigNode.c
+fraigPrime.c
+fraigSat.c
+fraigTable.c
+fraigUtil.c
+fraigVec.c
+csat_apis.c
+satMem.c
+satSolver.c
+satUtil.c
+fxu.c
+fxuCreate.c
+fxuHeapD.c
+fxuHeapS.c
+fxuList.c
+fxuMatrix.c
+fxuPair.c
+fxuPrint.c
+fxuReduce.c
+fxuSelect.c
+fxuSingle.c
+fxuUpdate.c
+rwrDec.c
+rwrEva.c
+rwrExp.c
+rwrLib.c
+rwrMan.c
+rwrPrint.c
+rwrTemp.c
+rwrUtil.c
+cutApi.c
+cutCut.c
+cutExpand.c
+cutMan.c
+cutMerge.c
+cutNode.c
+cutOracle.c
+cutPre22.c
+cutSeq.c
+cutTruth.c
+decAbc.c
+decFactor.c
+decMan.c
+decPrint.c
+decUtil.c
+simMan.c
+simSat.c
+simSeq.c
+simSupp.c
+simSwitch.c
+simSym.c
+simSymSat.c
+simSymSim.c
+simSymStr.c
+simUtils.c
+retArea.c
+retCore.c
+retDelay.c
+retFlow.c
+retIncrem.c
+retInit.c
+retLvalue.c
+fpga.c
+fpgaCore.c
+fpgaCreate.c
+fpgaCut.c
+fpgaCutUtils.c
+fpgaFanout.c
+fpgaLib.c
+fpgaMatch.c
+fpgaSwitch.c
+fpgaTime.c
+fpgaTruth.c
+fpgaUtils.c
+fpgaVec.c
+mapper.c
+mapperCanon.c
+mapperCore.c
+mapperCreate.c
+mapperCut.c
+mapperCutUtils.c
+mapperFanout.c
+mapperLib.c
+mapperMatch.c
+mapperRefs.c
+mapperSuper.c
+mapperSwitch.c
+mapperTable.c
+mapperTime.c
+mapperTree.c
+mapperTruth.c
+mapperUtils.c
+mapperVec.c
+mio.c
+mioApi.c
+mioFunc.c
+mioRead.c
+mioUtils.c
+super.c
+superAnd.c
+superGate.c
+superWrite.c
+ifCore.c
+ifCut.c
+ifMan.c
+ifMap.c
+ifReduce.c
+ifSeq.c
+ifTime.c
+ifTruth.c
+ifUtil.c
+extraBddAuto.c
+extraBddKmap.c
+extraBddMisc.c
+extraBddSymm.c
+extraBddUnate.c
+extraUtilBitMatrix.c
+extraUtilCanon.c
+extraUtilFile.c
+extraUtilMemory.c
+extraUtilMisc.c
+extraUtilProgress.c
+extraUtilReader.c
+extraUtilTruth.c
+extraUtilUtil.c
+st.c
+stmm.c
+mvc.c
+mvcApi.c
+mvcCompare.c
+mvcContain.c
+mvcCover.c
+mvcCube.c
+mvcDivide.c
+mvcDivisor.c
+mvcList.c
+mvcLits.c
+mvcMan.c
+mvcOpAlg.c
+mvcOpBool.c
+mvcPrint.c
+mvcSort.c
+mvcUtils.c
+cofactor.c
+c:\_projects\abc\src\misc\espresso\cofactor.c(370) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+cols.c
+compl.c
+c:\_projects\abc\src\misc\espresso\compl.c(200) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+c:\_projects\abc\src\misc\espresso\compl.c(201) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+contain.c
+c:\_projects\abc\src\misc\espresso\contain.c(221) : warning C4018: '!=' : signed/unsigned mismatch
+c:\_projects\abc\src\misc\espresso\contain.c(249) : warning C4018: '!=' : signed/unsigned mismatch
+c:\_projects\abc\src\misc\espresso\contain.c(338) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+cubehack.c
+cubestr.c
+cvrin.c
+C:\_projects\abc\src\misc\espresso\cvrin.c(38) : warning C4013: 'isspace' undefined; assuming extern returning int
+cvrm.c
+C:\_projects\abc\src\misc\espresso\cvrm.c(161) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+C:\_projects\abc\src\misc\espresso\cvrm.c(189) : warning C4113: 'int (__cdecl *)()' differs in parameter lists from 'int (__cdecl *)(const void *,const void *)'
+C:\_projects\abc\src\misc\espresso\cvrm.c(380) : warning C4033: 'foreach_output_function' must return a value
+C:\_projects\abc\src\misc\espresso\cvrm.c(391) : warning C4033: 'foreach_output_function' must return a value
+cvrmisc.c
+cvrout.c
+C:\_projects\abc\src\misc\espresso\cvrout.c(528) : warning C4033: 'output_symbolic_constraints' must return a value
+dominate.c
+C:\_projects\abc\src\misc\espresso\cvrout.c(453) : warning C4716: 'makeup_labels' : must return a value
+equiv.c
+espresso.c
+essen.c
+exact.c
+expand.c
+gasp.c
+gimpel.c
+globals.c
+hack.c
+C:\_projects\abc\src\misc\espresso\hack.c(21) : warning C4033: 'map_dcset' must return a value
+C:\_projects\abc\src\misc\espresso\hack.c(35) : warning C4033: 'map_dcset' must return a value
+C:\_projects\abc\src\misc\espresso\hack.c(420) : warning C4033: 'symbolic_hack_labels' must return a value
+indep.c
+irred.c
+map.c
+matrix.c
+mincov.c
+opo.c
+pair.c
+C:\_projects\abc\src\misc\espresso\pair.c(597) : warning C4033: 'generate_all_pairs' must return a value
+part.c
+C:\_projects\abc\src\misc\espresso\pair.c(456) : warning C4716: 'find_best_cost' : must return a value
+C:\_projects\abc\src\misc\espresso\pair.c(583) : warning C4716: 'minimize_pair' : must return a value
+C:\_projects\abc\src\misc\espresso\pair.c(675) : warning C4716: 'pair_free' : must return a value
+primes.c
+reduce.c
+rows.c
+set.c
+c:\_projects\abc\src\misc\espresso\set.c(453) : warning C4018: '<=' : signed/unsigned mismatch
+setc.c
+c:\_projects\abc\src\misc\espresso\set.c(27) : warning C4716: 'intcpy' : must return a value
+sharp.c
+sminterf.c
+solution.c
+sparse.c
+unate.c
+C:\_projects\abc\src\misc\espresso\unate.c(172) : warning C4018: '<' : signed/unsigned mismatch
+C:\_projects\abc\src\misc\espresso\unate.c(175) : warning C4018: '==' : signed/unsigned mismatch
+verify.c
+nmApi.c
+nmTable.c
+hopBalance.c
+hopCheck.c
+hopDfs.c
+hopMan.c
+hopMem.c
+hopObj.c
+hopOper.c
+hopTable.c
+hopUtil.c
+ivyBalance.c
+ivyCanon.c
+ivyCheck.c
+ivyCut.c
+ivyCutTrav.c
+ivyDfs.c
+ivyDsd.c
+ivyFanout.c
+ivyFastMap.c
+ivyFraig.c
+ivyHaig.c
+ivyMan.c
+ivyMem.c
+ivyMulti.c
+ivyObj.c
+ivyOper.c
+ivyResyn.c
+ivyRwr.c
+ivySeq.c
+ivyShow.c
+ivyTable.c
+ivyUtil.c
+rwtDec.c
+rwtMan.c
+rwtUtil.c
+mem.c
+abcHie.c
+abcBlifMv.c
+abcCas.c
+abcDar.c
+abcHaig.c
+abcMeasure.c
+abcOdc.c
+abcPart.c
+abcRec.c
+abcQbf.c
+abcQuant.c
+ioReadDsd.c
+ioReadBlifMv.c
+ioReadVerilog.c
+ioWriteVerilog.c
+ioWriteBlifMv.c
+casDec.c
+casCore.c
+pr.c
+satTrace.c
+satInter.c
+satStore.c
+extraBddCas.c
+ioaWriteAig.c
+ioaReadAig.c
+ioaUtil.c
+darBalance.c
+darCore.c
+darCut.c
+darData.c
+darLib.c
+darMan.c
+darPrec.c
+darRefact.c
+darResub.c
+darScript.c
+fraBmc.c
+fraCec.c
+fraClass.c
+fraCnf.c
+fraCore.c
+fraImp.c
+fraInd.c
+fraLcr.c
+fraMan.c
+fraPart.c
+fraSat.c
+fraSec.c
+fraSim.c
+cnfCore.c
+cnfCut.c
+cnfData.c
+cnfMan.c
+cnfMap.c
+cnfPost.c
+cnfUtil.c
+cnfWrite.c
+cswCore.c
+cswCut.c
+cswMan.c
+cswTable.c
+cloud.c
+kitAig.c
+kitBdd.c
+kitCloud.c
+kitDsd.c
+kitFactor.c
+kitGraph.c
+kitHop.c
+kitIsop.c
+kitSop.c
+kitTruth.c
+bdcCore.c
+bdcDec.c
+bdcTable.c
+aigCheck.c
+aigDfs.c
+aigFanout.c
+aigMan.c
+aigMem.c
+aigMffc.c
+aigObj.c
+aigOper.c
+aigOrder.c
+aigPart.c
+aigRepr.c
+aigRet.c
+aigScl.c
+aigSeq.c
+aigShow.c
+aigTable.c
+aigTime.c
+aigTiming.c
+aigTruth.c
+aigTsim.c
+aigUtil.c
+aigWin.c
+bar.c
+resCore.c
+resDivs.c
+resFilter.c
+resSat.c
+resSim.c
+resStrash.c
+resWin.c
+lpkAbcDec.c
+lpkAbcDsd.c
+lpkAbcMux.c
+lpkAbcUtil.c
+lpkCore.c
+lpkCut.c
+lpkMan.c
+lpkMap.c
+lpkMulti.c
+lpkMux.c
+lpkSets.c
+Creating library...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AD.tmp" with contents
+[
+/nologo /o"abclib\DebugLib/abclib.bsc" 
+.\abclib\DebugLib\abcAig.sbr
+.\abclib\DebugLib\abcCheck.sbr
+.\abclib\DebugLib\abcDfs.sbr
+.\abclib\DebugLib\abcFanio.sbr
+.\abclib\DebugLib\abcFunc.sbr
+.\abclib\DebugLib\abcLatch.sbr
+.\abclib\DebugLib\abcLib.sbr
+.\abclib\DebugLib\abcMinBase.sbr
+.\abclib\DebugLib\abcNames.sbr
+.\abclib\DebugLib\abcNetlist.sbr
+.\abclib\DebugLib\abcNtk.sbr
+.\abclib\DebugLib\abcObj.sbr
+.\abclib\DebugLib\abcRefs.sbr
+.\abclib\DebugLib\abcShow.sbr
+.\abclib\DebugLib\abcSop.sbr
+.\abclib\DebugLib\abcUtil.sbr
+.\abclib\DebugLib\abc.sbr
+.\abclib\DebugLib\abcAttach.sbr
+.\abclib\DebugLib\abcAuto.sbr
+.\abclib\DebugLib\abcBalance.sbr
+.\abclib\DebugLib\abcBmc.sbr
+.\abclib\DebugLib\abcClpBdd.sbr
+.\abclib\DebugLib\abcClpSop.sbr
+.\abclib\DebugLib\abcCut.sbr
+.\abclib\DebugLib\abcDebug.sbr
+.\abclib\DebugLib\abcDress.sbr
+.\abclib\DebugLib\abcDsd.sbr
+.\abclib\DebugLib\abcEspresso.sbr
+.\abclib\DebugLib\abcExtract.sbr
+.\abclib\DebugLib\abcFpga.sbr
+.\abclib\DebugLib\abcFpgaFast.sbr
+.\abclib\DebugLib\abcFraig.sbr
+.\abclib\DebugLib\abcFxu.sbr
+.\abclib\DebugLib\abcGen.sbr
+.\abclib\DebugLib\abcIf.sbr
+.\abclib\DebugLib\abcIvy.sbr
+.\abclib\DebugLib\abcLut.sbr
+.\abclib\DebugLib\abcMap.sbr
+.\abclib\DebugLib\abcMini.sbr
+.\abclib\DebugLib\abcMiter.sbr
+.\abclib\DebugLib\abcMulti.sbr
+.\abclib\DebugLib\abcMv.sbr
+.\abclib\DebugLib\abcNtbdd.sbr
+.\abclib\DebugLib\abcOrder.sbr
+.\abclib\DebugLib\abcPrint.sbr
+.\abclib\DebugLib\abcProve.sbr
+.\abclib\DebugLib\abcReconv.sbr
+.\abclib\DebugLib\abcRefactor.sbr
+.\abclib\DebugLib\abcRenode.sbr
+.\abclib\DebugLib\abcReorder.sbr
+.\abclib\DebugLib\abcRestruct.sbr
+.\abclib\DebugLib\abcResub.sbr
+.\abclib\DebugLib\abcRewrite.sbr
+.\abclib\DebugLib\abcRr.sbr
+.\abclib\DebugLib\abcSat.sbr
+.\abclib\DebugLib\abcStrash.sbr
+.\abclib\DebugLib\abcSweep.sbr
+.\abclib\DebugLib\abcSymm.sbr
+.\abclib\DebugLib\abcTiming.sbr
+.\abclib\DebugLib\abcUnate.sbr
+.\abclib\DebugLib\abcUnreach.sbr
+.\abclib\DebugLib\abcVerify.sbr
+.\abclib\DebugLib\abcXsim.sbr
+.\abclib\DebugLib\cmd.sbr
+.\abclib\DebugLib\cmdAlias.sbr
+.\abclib\DebugLib\cmdApi.sbr
+.\abclib\DebugLib\cmdFlag.sbr
+.\abclib\DebugLib\cmdHist.sbr
+.\abclib\DebugLib\cmdUtils.sbr
+.\abclib\DebugLib\io.sbr
+.\abclib\DebugLib\ioReadAiger.sbr
+.\abclib\DebugLib\ioReadBaf.sbr
+.\abclib\DebugLib\ioReadBench.sbr
+.\abclib\DebugLib\ioReadBlif.sbr
+.\abclib\DebugLib\ioReadBlifAig.sbr
+.\abclib\DebugLib\ioReadEdif.sbr
+.\abclib\DebugLib\ioReadEqn.sbr
+.\abclib\DebugLib\ioReadPla.sbr
+.\abclib\DebugLib\ioUtil.sbr
+.\abclib\DebugLib\ioWriteAiger.sbr
+.\abclib\DebugLib\ioWriteBaf.sbr
+.\abclib\DebugLib\ioWriteBench.sbr
+.\abclib\DebugLib\ioWriteBlif.sbr
+.\abclib\DebugLib\ioWriteCnf.sbr
+.\abclib\DebugLib\ioWriteDot.sbr
+.\abclib\DebugLib\ioWriteEqn.sbr
+.\abclib\DebugLib\ioWriteGml.sbr
+.\abclib\DebugLib\ioWriteList.sbr
+.\abclib\DebugLib\ioWritePla.sbr
+.\abclib\DebugLib\libSupport.sbr
+.\abclib\DebugLib\main.sbr
+.\abclib\DebugLib\mainFrame.sbr
+.\abclib\DebugLib\mainInit.sbr
+.\abclib\DebugLib\mainUtils.sbr
+.\abclib\DebugLib\verCore.sbr
+.\abclib\DebugLib\verFormula.sbr
+.\abclib\DebugLib\verParse.sbr
+.\abclib\DebugLib\verStream.sbr
+.\abclib\DebugLib\cuddAddAbs.sbr
+.\abclib\DebugLib\cuddAddApply.sbr
+.\abclib\DebugLib\cuddAddFind.sbr
+.\abclib\DebugLib\cuddAddInv.sbr
+.\abclib\DebugLib\cuddAddIte.sbr
+.\abclib\DebugLib\cuddAddNeg.sbr
+.\abclib\DebugLib\cuddAddWalsh.sbr
+.\abclib\DebugLib\cuddAndAbs.sbr
+.\abclib\DebugLib\cuddAnneal.sbr
+.\abclib\DebugLib\cuddApa.sbr
+.\abclib\DebugLib\cuddAPI.sbr
+.\abclib\DebugLib\cuddApprox.sbr
+.\abclib\DebugLib\cuddBddAbs.sbr
+.\abclib\DebugLib\cuddBddCorr.sbr
+.\abclib\DebugLib\cuddBddIte.sbr
+.\abclib\DebugLib\cuddBridge.sbr
+.\abclib\DebugLib\cuddCache.sbr
+.\abclib\DebugLib\cuddCheck.sbr
+.\abclib\DebugLib\cuddClip.sbr
+.\abclib\DebugLib\cuddCof.sbr
+.\abclib\DebugLib\cuddCompose.sbr
+.\abclib\DebugLib\cuddDecomp.sbr
+.\abclib\DebugLib\cuddEssent.sbr
+.\abclib\DebugLib\cuddExact.sbr
+.\abclib\DebugLib\cuddExport.sbr
+.\abclib\DebugLib\cuddGenCof.sbr
+.\abclib\DebugLib\cuddGenetic.sbr
+.\abclib\DebugLib\cuddGroup.sbr
+.\abclib\DebugLib\cuddHarwell.sbr
+.\abclib\DebugLib\cuddInit.sbr
+.\abclib\DebugLib\cuddInteract.sbr
+.\abclib\DebugLib\cuddLCache.sbr
+.\abclib\DebugLib\cuddLevelQ.sbr
+.\abclib\DebugLib\cuddLinear.sbr
+.\abclib\DebugLib\cuddLiteral.sbr
+.\abclib\DebugLib\cuddMatMult.sbr
+.\abclib\DebugLib\cuddPriority.sbr
+.\abclib\DebugLib\cuddRead.sbr
+.\abclib\DebugLib\cuddRef.sbr
+.\abclib\DebugLib\cuddReorder.sbr
+.\abclib\DebugLib\cuddSat.sbr
+.\abclib\DebugLib\cuddSign.sbr
+.\abclib\DebugLib\cuddSolve.sbr
+.\abclib\DebugLib\cuddSplit.sbr
+.\abclib\DebugLib\cuddSubsetHB.sbr
+.\abclib\DebugLib\cuddSubsetSP.sbr
+.\abclib\DebugLib\cuddSymmetry.sbr
+.\abclib\DebugLib\cuddTable.sbr
+.\abclib\DebugLib\cuddUtil.sbr
+.\abclib\DebugLib\cuddWindow.sbr
+.\abclib\DebugLib\cuddZddCount.sbr
+.\abclib\DebugLib\cuddZddFuncs.sbr
+.\abclib\DebugLib\cuddZddGroup.sbr
+.\abclib\DebugLib\cuddZddIsop.sbr
+.\abclib\DebugLib\cuddZddLin.sbr
+.\abclib\DebugLib\cuddZddMisc.sbr
+.\abclib\DebugLib\cuddZddPort.sbr
+.\abclib\DebugLib\cuddZddReord.sbr
+.\abclib\DebugLib\cuddZddSetop.sbr
+.\abclib\DebugLib\cuddZddSymm.sbr
+.\abclib\DebugLib\cuddZddUtil.sbr
+.\abclib\DebugLib\epd.sbr
+.\abclib\DebugLib\mtrBasic.sbr
+.\abclib\DebugLib\mtrGroup.sbr
+.\abclib\DebugLib\parseCore.sbr
+.\abclib\DebugLib\parseEqn.sbr
+.\abclib\DebugLib\parseStack.sbr
+.\abclib\DebugLib\dsdApi.sbr
+.\abclib\DebugLib\dsdCheck.sbr
+.\abclib\DebugLib\dsdLocal.sbr
+.\abclib\DebugLib\dsdMan.sbr
+.\abclib\DebugLib\dsdProc.sbr
+.\abclib\DebugLib\dsdTree.sbr
+.\abclib\DebugLib\reoApi.sbr
+.\abclib\DebugLib\reoCore.sbr
+.\abclib\DebugLib\reoProfile.sbr
+.\abclib\DebugLib\reoSift.sbr
+.\abclib\DebugLib\reoSwap.sbr
+.\abclib\DebugLib\reoTest.sbr
+.\abclib\DebugLib\reoTransfer.sbr
+.\abclib\DebugLib\reoUnits.sbr
+.\abclib\DebugLib\msatActivity.sbr
+.\abclib\DebugLib\msatClause.sbr
+.\abclib\DebugLib\msatClauseVec.sbr
+.\abclib\DebugLib\msatMem.sbr
+.\abclib\DebugLib\msatOrderH.sbr
+.\abclib\DebugLib\msatQueue.sbr
+.\abclib\DebugLib\msatRead.sbr
+.\abclib\DebugLib\msatSolverApi.sbr
+.\abclib\DebugLib\msatSolverCore.sbr
+.\abclib\DebugLib\msatSolverIo.sbr
+.\abclib\DebugLib\msatSolverSearch.sbr
+.\abclib\DebugLib\msatSort.sbr
+.\abclib\DebugLib\msatVec.sbr
+.\abclib\DebugLib\fraigApi.sbr
+.\abclib\DebugLib\fraigCanon.sbr
+.\abclib\DebugLib\fraigChoice.sbr
+.\abclib\DebugLib\fraigFanout.sbr
+.\abclib\DebugLib\fraigFeed.sbr
+.\abclib\DebugLib\fraigMan.sbr
+.\abclib\DebugLib\fraigMem.sbr
+.\abclib\DebugLib\fraigNode.sbr
+.\abclib\DebugLib\fraigPrime.sbr
+.\abclib\DebugLib\fraigSat.sbr
+.\abclib\DebugLib\fraigTable.sbr
+.\abclib\DebugLib\fraigUtil.sbr
+.\abclib\DebugLib\fraigVec.sbr
+.\abclib\DebugLib\csat_apis.sbr
+.\abclib\DebugLib\satMem.sbr
+.\abclib\DebugLib\satSolver.sbr
+.\abclib\DebugLib\satUtil.sbr
+.\abclib\DebugLib\fxu.sbr
+.\abclib\DebugLib\fxuCreate.sbr
+.\abclib\DebugLib\fxuHeapD.sbr
+.\abclib\DebugLib\fxuHeapS.sbr
+.\abclib\DebugLib\fxuList.sbr
+.\abclib\DebugLib\fxuMatrix.sbr
+.\abclib\DebugLib\fxuPair.sbr
+.\abclib\DebugLib\fxuPrint.sbr
+.\abclib\DebugLib\fxuReduce.sbr
+.\abclib\DebugLib\fxuSelect.sbr
+.\abclib\DebugLib\fxuSingle.sbr
+.\abclib\DebugLib\fxuUpdate.sbr
+.\abclib\DebugLib\rwrDec.sbr
+.\abclib\DebugLib\rwrEva.sbr
+.\abclib\DebugLib\rwrExp.sbr
+.\abclib\DebugLib\rwrLib.sbr
+.\abclib\DebugLib\rwrMan.sbr
+.\abclib\DebugLib\rwrPrint.sbr
+.\abclib\DebugLib\rwrTemp.sbr
+.\abclib\DebugLib\rwrUtil.sbr
+.\abclib\DebugLib\cutApi.sbr
+.\abclib\DebugLib\cutCut.sbr
+.\abclib\DebugLib\cutExpand.sbr
+.\abclib\DebugLib\cutMan.sbr
+.\abclib\DebugLib\cutMerge.sbr
+.\abclib\DebugLib\cutNode.sbr
+.\abclib\DebugLib\cutOracle.sbr
+.\abclib\DebugLib\cutPre22.sbr
+.\abclib\DebugLib\cutSeq.sbr
+.\abclib\DebugLib\cutTruth.sbr
+.\abclib\DebugLib\decAbc.sbr
+.\abclib\DebugLib\decFactor.sbr
+.\abclib\DebugLib\decMan.sbr
+.\abclib\DebugLib\decPrint.sbr
+.\abclib\DebugLib\decUtil.sbr
+.\abclib\DebugLib\simMan.sbr
+.\abclib\DebugLib\simSat.sbr
+.\abclib\DebugLib\simSeq.sbr
+.\abclib\DebugLib\simSupp.sbr
+.\abclib\DebugLib\simSwitch.sbr
+.\abclib\DebugLib\simSym.sbr
+.\abclib\DebugLib\simSymSat.sbr
+.\abclib\DebugLib\simSymSim.sbr
+.\abclib\DebugLib\simSymStr.sbr
+.\abclib\DebugLib\simUtils.sbr
+.\abclib\DebugLib\retArea.sbr
+.\abclib\DebugLib\retCore.sbr
+.\abclib\DebugLib\retDelay.sbr
+.\abclib\DebugLib\retFlow.sbr
+.\abclib\DebugLib\retIncrem.sbr
+.\abclib\DebugLib\retInit.sbr
+.\abclib\DebugLib\retLvalue.sbr
+.\abclib\DebugLib\fpga.sbr
+.\abclib\DebugLib\fpgaCore.sbr
+.\abclib\DebugLib\fpgaCreate.sbr
+.\abclib\DebugLib\fpgaCut.sbr
+.\abclib\DebugLib\fpgaCutUtils.sbr
+.\abclib\DebugLib\fpgaFanout.sbr
+.\abclib\DebugLib\fpgaLib.sbr
+.\abclib\DebugLib\fpgaMatch.sbr
+.\abclib\DebugLib\fpgaSwitch.sbr
+.\abclib\DebugLib\fpgaTime.sbr
+.\abclib\DebugLib\fpgaTruth.sbr
+.\abclib\DebugLib\fpgaUtils.sbr
+.\abclib\DebugLib\fpgaVec.sbr
+.\abclib\DebugLib\mapper.sbr
+.\abclib\DebugLib\mapperCanon.sbr
+.\abclib\DebugLib\mapperCore.sbr
+.\abclib\DebugLib\mapperCreate.sbr
+.\abclib\DebugLib\mapperCut.sbr
+.\abclib\DebugLib\mapperCutUtils.sbr
+.\abclib\DebugLib\mapperFanout.sbr
+.\abclib\DebugLib\mapperLib.sbr
+.\abclib\DebugLib\mapperMatch.sbr
+.\abclib\DebugLib\mapperRefs.sbr
+.\abclib\DebugLib\mapperSuper.sbr
+.\abclib\DebugLib\mapperSwitch.sbr
+.\abclib\DebugLib\mapperTable.sbr
+.\abclib\DebugLib\mapperTime.sbr
+.\abclib\DebugLib\mapperTree.sbr
+.\abclib\DebugLib\mapperTruth.sbr
+.\abclib\DebugLib\mapperUtils.sbr
+.\abclib\DebugLib\mapperVec.sbr
+.\abclib\DebugLib\mio.sbr
+.\abclib\DebugLib\mioApi.sbr
+.\abclib\DebugLib\mioFunc.sbr
+.\abclib\DebugLib\mioRead.sbr
+.\abclib\DebugLib\mioUtils.sbr
+.\abclib\DebugLib\super.sbr
+.\abclib\DebugLib\superAnd.sbr
+.\abclib\DebugLib\superGate.sbr
+.\abclib\DebugLib\superWrite.sbr
+.\abclib\DebugLib\ifCore.sbr
+.\abclib\DebugLib\ifCut.sbr
+.\abclib\DebugLib\ifMan.sbr
+.\abclib\DebugLib\ifMap.sbr
+.\abclib\DebugLib\ifReduce.sbr
+.\abclib\DebugLib\ifSeq.sbr
+.\abclib\DebugLib\ifTime.sbr
+.\abclib\DebugLib\ifTruth.sbr
+.\abclib\DebugLib\ifUtil.sbr
+.\abclib\DebugLib\extraBddAuto.sbr
+.\abclib\DebugLib\extraBddKmap.sbr
+.\abclib\DebugLib\extraBddMisc.sbr
+.\abclib\DebugLib\extraBddSymm.sbr
+.\abclib\DebugLib\extraBddUnate.sbr
+.\abclib\DebugLib\extraUtilBitMatrix.sbr
+.\abclib\DebugLib\extraUtilCanon.sbr
+.\abclib\DebugLib\extraUtilFile.sbr
+.\abclib\DebugLib\extraUtilMemory.sbr
+.\abclib\DebugLib\extraUtilMisc.sbr
+.\abclib\DebugLib\extraUtilProgress.sbr
+.\abclib\DebugLib\extraUtilReader.sbr
+.\abclib\DebugLib\extraUtilTruth.sbr
+.\abclib\DebugLib\extraUtilUtil.sbr
+.\abclib\DebugLib\st.sbr
+.\abclib\DebugLib\stmm.sbr
+.\abclib\DebugLib\mvc.sbr
+.\abclib\DebugLib\mvcApi.sbr
+.\abclib\DebugLib\mvcCompare.sbr
+.\abclib\DebugLib\mvcContain.sbr
+.\abclib\DebugLib\mvcCover.sbr
+.\abclib\DebugLib\mvcCube.sbr
+.\abclib\DebugLib\mvcDivide.sbr
+.\abclib\DebugLib\mvcDivisor.sbr
+.\abclib\DebugLib\mvcList.sbr
+.\abclib\DebugLib\mvcLits.sbr
+.\abclib\DebugLib\mvcMan.sbr
+.\abclib\DebugLib\mvcOpAlg.sbr
+.\abclib\DebugLib\mvcOpBool.sbr
+.\abclib\DebugLib\mvcPrint.sbr
+.\abclib\DebugLib\mvcSort.sbr
+.\abclib\DebugLib\mvcUtils.sbr
+.\abclib\DebugLib\cofactor.sbr
+.\abclib\DebugLib\cols.sbr
+.\abclib\DebugLib\compl.sbr
+.\abclib\DebugLib\contain.sbr
+.\abclib\DebugLib\cubehack.sbr
+.\abclib\DebugLib\cubestr.sbr
+.\abclib\DebugLib\cvrin.sbr
+.\abclib\DebugLib\cvrm.sbr
+.\abclib\DebugLib\cvrmisc.sbr
+.\abclib\DebugLib\cvrout.sbr
+.\abclib\DebugLib\dominate.sbr
+.\abclib\DebugLib\equiv.sbr
+.\abclib\DebugLib\espresso.sbr
+.\abclib\DebugLib\essen.sbr
+.\abclib\DebugLib\exact.sbr
+.\abclib\DebugLib\expand.sbr
+.\abclib\DebugLib\gasp.sbr
+.\abclib\DebugLib\gimpel.sbr
+.\abclib\DebugLib\globals.sbr
+.\abclib\DebugLib\hack.sbr
+.\abclib\DebugLib\indep.sbr
+.\abclib\DebugLib\irred.sbr
+.\abclib\DebugLib\map.sbr
+.\abclib\DebugLib\matrix.sbr
+.\abclib\DebugLib\mincov.sbr
+.\abclib\DebugLib\opo.sbr
+.\abclib\DebugLib\pair.sbr
+.\abclib\DebugLib\part.sbr
+.\abclib\DebugLib\primes.sbr
+.\abclib\DebugLib\reduce.sbr
+.\abclib\DebugLib\rows.sbr
+.\abclib\DebugLib\set.sbr
+.\abclib\DebugLib\setc.sbr
+.\abclib\DebugLib\sharp.sbr
+.\abclib\DebugLib\sminterf.sbr
+.\abclib\DebugLib\solution.sbr
+.\abclib\DebugLib\sparse.sbr
+.\abclib\DebugLib\unate.sbr
+.\abclib\DebugLib\verify.sbr
+.\abclib\DebugLib\nmApi.sbr
+.\abclib\DebugLib\nmTable.sbr
+.\abclib\DebugLib\hopBalance.sbr
+.\abclib\DebugLib\hopCheck.sbr
+.\abclib\DebugLib\hopDfs.sbr
+.\abclib\DebugLib\hopMan.sbr
+.\abclib\DebugLib\hopMem.sbr
+.\abclib\DebugLib\hopObj.sbr
+.\abclib\DebugLib\hopOper.sbr
+.\abclib\DebugLib\hopTable.sbr
+.\abclib\DebugLib\hopUtil.sbr
+.\abclib\DebugLib\ivyBalance.sbr
+.\abclib\DebugLib\ivyCanon.sbr
+.\abclib\DebugLib\ivyCheck.sbr
+.\abclib\DebugLib\ivyCut.sbr
+.\abclib\DebugLib\ivyCutTrav.sbr
+.\abclib\DebugLib\ivyDfs.sbr
+.\abclib\DebugLib\ivyDsd.sbr
+.\abclib\DebugLib\ivyFanout.sbr
+.\abclib\DebugLib\ivyFastMap.sbr
+.\abclib\DebugLib\ivyFraig.sbr
+.\abclib\DebugLib\ivyHaig.sbr
+.\abclib\DebugLib\ivyMan.sbr
+.\abclib\DebugLib\ivyMem.sbr
+.\abclib\DebugLib\ivyMulti.sbr
+.\abclib\DebugLib\ivyObj.sbr
+.\abclib\DebugLib\ivyOper.sbr
+.\abclib\DebugLib\ivyResyn.sbr
+.\abclib\DebugLib\ivyRwr.sbr
+.\abclib\DebugLib\ivySeq.sbr
+.\abclib\DebugLib\ivyShow.sbr
+.\abclib\DebugLib\ivyTable.sbr
+.\abclib\DebugLib\ivyUtil.sbr
+.\abclib\DebugLib\rwtDec.sbr
+.\abclib\DebugLib\rwtMan.sbr
+.\abclib\DebugLib\rwtUtil.sbr
+.\abclib\DebugLib\mem.sbr
+.\abclib\DebugLib\abcHie.sbr
+.\abclib\DebugLib\abcBlifMv.sbr
+.\abclib\DebugLib\abcCas.sbr
+.\abclib\DebugLib\abcDar.sbr
+.\abclib\DebugLib\abcHaig.sbr
+.\abclib\DebugLib\abcMeasure.sbr
+.\abclib\DebugLib\abcOdc.sbr
+.\abclib\DebugLib\abcPart.sbr
+.\abclib\DebugLib\abcRec.sbr
+.\abclib\DebugLib\abcQbf.sbr
+.\abclib\DebugLib\abcQuant.sbr
+.\abclib\DebugLib\ioReadDsd.sbr
+.\abclib\DebugLib\ioReadBlifMv.sbr
+.\abclib\DebugLib\ioReadVerilog.sbr
+.\abclib\DebugLib\ioWriteVerilog.sbr
+.\abclib\DebugLib\ioWriteBlifMv.sbr
+.\abclib\DebugLib\casDec.sbr
+.\abclib\DebugLib\casCore.sbr
+.\abclib\DebugLib\pr.sbr
+.\abclib\DebugLib\satTrace.sbr
+.\abclib\DebugLib\satInter.sbr
+.\abclib\DebugLib\satStore.sbr
+.\abclib\DebugLib\extraBddCas.sbr
+.\abclib\DebugLib\ioaWriteAig.sbr
+.\abclib\DebugLib\ioaReadAig.sbr
+.\abclib\DebugLib\ioaUtil.sbr
+.\abclib\DebugLib\darBalance.sbr
+.\abclib\DebugLib\darCore.sbr
+.\abclib\DebugLib\darCut.sbr
+.\abclib\DebugLib\darData.sbr
+.\abclib\DebugLib\darLib.sbr
+.\abclib\DebugLib\darMan.sbr
+.\abclib\DebugLib\darPrec.sbr
+.\abclib\DebugLib\darRefact.sbr
+.\abclib\DebugLib\darResub.sbr
+.\abclib\DebugLib\darScript.sbr
+.\abclib\DebugLib\fraBmc.sbr
+.\abclib\DebugLib\fraCec.sbr
+.\abclib\DebugLib\fraClass.sbr
+.\abclib\DebugLib\fraCnf.sbr
+.\abclib\DebugLib\fraCore.sbr
+.\abclib\DebugLib\fraImp.sbr
+.\abclib\DebugLib\fraInd.sbr
+.\abclib\DebugLib\fraLcr.sbr
+.\abclib\DebugLib\fraMan.sbr
+.\abclib\DebugLib\fraPart.sbr
+.\abclib\DebugLib\fraSat.sbr
+.\abclib\DebugLib\fraSec.sbr
+.\abclib\DebugLib\fraSim.sbr
+.\abclib\DebugLib\cnfCore.sbr
+.\abclib\DebugLib\cnfCut.sbr
+.\abclib\DebugLib\cnfData.sbr
+.\abclib\DebugLib\cnfMan.sbr
+.\abclib\DebugLib\cnfMap.sbr
+.\abclib\DebugLib\cnfPost.sbr
+.\abclib\DebugLib\cnfUtil.sbr
+.\abclib\DebugLib\cnfWrite.sbr
+.\abclib\DebugLib\cswCore.sbr
+.\abclib\DebugLib\cswCut.sbr
+.\abclib\DebugLib\cswMan.sbr
+.\abclib\DebugLib\cswTable.sbr
+.\abclib\DebugLib\cloud.sbr
+.\abclib\DebugLib\kitAig.sbr
+.\abclib\DebugLib\kitBdd.sbr
+.\abclib\DebugLib\kitCloud.sbr
+.\abclib\DebugLib\kitDsd.sbr
+.\abclib\DebugLib\kitFactor.sbr
+.\abclib\DebugLib\kitGraph.sbr
+.\abclib\DebugLib\kitHop.sbr
+.\abclib\DebugLib\kitIsop.sbr
+.\abclib\DebugLib\kitSop.sbr
+.\abclib\DebugLib\kitTruth.sbr
+.\abclib\DebugLib\bdcCore.sbr
+.\abclib\DebugLib\bdcDec.sbr
+.\abclib\DebugLib\bdcTable.sbr
+.\abclib\DebugLib\aigCheck.sbr
+.\abclib\DebugLib\aigDfs.sbr
+.\abclib\DebugLib\aigFanout.sbr
+.\abclib\DebugLib\aigMan.sbr
+.\abclib\DebugLib\aigMem.sbr
+.\abclib\DebugLib\aigMffc.sbr
+.\abclib\DebugLib\aigObj.sbr
+.\abclib\DebugLib\aigOper.sbr
+.\abclib\DebugLib\aigOrder.sbr
+.\abclib\DebugLib\aigPart.sbr
+.\abclib\DebugLib\aigRepr.sbr
+.\abclib\DebugLib\aigRet.sbr
+.\abclib\DebugLib\aigScl.sbr
+.\abclib\DebugLib\aigSeq.sbr
+.\abclib\DebugLib\aigShow.sbr
+.\abclib\DebugLib\aigTable.sbr
+.\abclib\DebugLib\aigTime.sbr
+.\abclib\DebugLib\aigTiming.sbr
+.\abclib\DebugLib\aigTruth.sbr
+.\abclib\DebugLib\aigTsim.sbr
+.\abclib\DebugLib\aigUtil.sbr
+.\abclib\DebugLib\aigWin.sbr
+.\abclib\DebugLib\bar.sbr
+.\abclib\DebugLib\resCore.sbr
+.\abclib\DebugLib\resDivs.sbr
+.\abclib\DebugLib\resFilter.sbr
+.\abclib\DebugLib\resSat.sbr
+.\abclib\DebugLib\resSim.sbr
+.\abclib\DebugLib\resStrash.sbr
+.\abclib\DebugLib\resWin.sbr
+.\abclib\DebugLib\lpkAbcDec.sbr
+.\abclib\DebugLib\lpkAbcDsd.sbr
+.\abclib\DebugLib\lpkAbcMux.sbr
+.\abclib\DebugLib\lpkAbcUtil.sbr
+.\abclib\DebugLib\lpkCore.sbr
+.\abclib\DebugLib\lpkCut.sbr
+.\abclib\DebugLib\lpkMan.sbr
+.\abclib\DebugLib\lpkMap.sbr
+.\abclib\DebugLib\lpkMulti.sbr
+.\abclib\DebugLib\lpkMux.sbr
+.\abclib\DebugLib\lpkSets.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20AD.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
+
+
+
+<h3>Results</h3>
+abclib_debug.lib - 0 error(s), 37 warning(s)
+</pre>
+</body>
+</html>
diff --git a/abctestlib.plg b/abctestlib.plg
new file mode 100644
index 00000000..4bf69035
--- /dev/null
+++ b/abctestlib.plg
@@ -0,0 +1,32 @@
+<html>
+<body>
+<pre>
+<h1>Build Log</h1>
+<h3>
+--------------------Configuration: abctestlib - Win32 Release--------------------
+</h3>
+<h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B8.tmp" with contents
+[
+/nologo /ML /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /Fp"Release/abctestlib.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
+"C:\_projects\abc\demo.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B8.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B9.tmp" with contents
+[
+kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_release.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abctestlib.pdb" /machine:I386 /out:"_TEST/abctestlib.exe" 
+.\Release\demo.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B9.tmp"
+<h3>Output Window</h3>
+Compiling...
+demo.c
+Linking...
+
+
+
+<h3>Results</h3>
+abctestlib.exe - 0 error(s), 0 warning(s)
+</pre>
+</body>
+</html>
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 12151343..cd810b5e 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -471,6 +471,7 @@ extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Obj_t *     Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
+extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 1979f4f9..57032703 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -217,6 +217,40 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        assert( !Aig_ObjIsBuf(pObj) );
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Extracts the miter composed of XOR of the two nodes.]
 
   Description []
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 7929b25d..a35e1169 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1496,6 +1496,79 @@ void Fra_ClausPrintIndClauses( Clu_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes the clauses into an AIGER file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
+{
+    Aig_Obj_t * pLiteral;
+    int NodeId = pVar2Id[ lit_var(Lit) ];
+    assert( NodeId >= 0 );
+    pLiteral = Aig_ManObj( p->pAig, NodeId )->pData;
+    return Aig_NotCond( pLiteral, lit_sign(Lit) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the clauses into an AIGER file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausWriteIndClauses( Clu_Man_t * p )
+{
+    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pClause, * pLiteral;
+    char Buffer[500];
+    int * pStart, * pVar2Id; 
+    int Beg, End, i, k;
+    // create mapping from SAT vars to node IDs
+    pVar2Id = ALLOC( int, p->pCnf->nVars );
+    memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
+    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
+        if ( p->pCnf->pVarNums[i] >= 0 )
+        {
+            assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
+            pVar2Id[ p->pCnf->pVarNums[i] ] = i;
+        }
+    // start the manager
+    pNew = Aig_ManDupWithoutPos( p->pAig );
+    // add the clauses
+    Beg = 0;
+    pStart = Vec_IntArray( p->vLitsProven );
+    Vec_IntForEachEntry( p->vClausesProven, End, i )
+    {
+        pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
+        for ( k = Beg + 1; k < End; k++ )
+        {
+            pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
+            pClause = Aig_Or( pNew, pClause, pLiteral );
+        }
+        Aig_ObjCreatePo( pNew, pClause );
+        Beg = End;
+    }
+    free( pVar2Id );
+    Aig_ManCleanup( pNew );
+    // write the manager into a file
+    sprintf( Buffer, "%s_care.aig", p->pAig->pName );
+    printf( "Care clauses are written into file \"%s\".\n", Buffer );
+    Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+    Aig_ManStop( pNew );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the clause holds using the given simulation info.]
 
   Description []
@@ -1751,6 +1824,11 @@ clk = clock();
         Fra_ClausPrintIndClauses( p );
         Fra_ClausEstimateCoverage( p );
     }
+
+    if ( !p->fTarget )
+    {
+        Fra_ClausWriteIndClauses( p );
+    }
 /*
     // print the statistic into a file
     {
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 6783b459..4a3f9b03 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -395,25 +395,28 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj1, * pObj2, * pObj;
-    int i, Out1, Out2;
+    int i, Out1, Out2, nTruePis;
     pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
-    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+//    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+//        Aig_ObjCreatePi(pNew);
+    Aig_ManForEachPi( p->pManAig, pObj, i )
         Aig_ObjCreatePi(pNew);
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( pNew, Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( pNew, Fra_LitReg(Out2) );
+        pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) );
         pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
         pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
         pObj  = Aig_Or( pNew, pObj1, pObj2 );
         Aig_ObjCreatePo( pNew, pObj );
     }
     Aig_ManCleanup(pNew);
-    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
+//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
     return pNew;
 }
 
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index f345b6d1..07044b52 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -470,8 +470,16 @@ clk2 = clock();
 clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
+        extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+        char Buffer[500];
+        Aig_Man_t * pNew;
         pManAigNew = Aig_ManDup( pManAig, 1 );
-        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
+//        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
+        pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
+        sprintf( Buffer, "%s_care.aig", p->pManAig->pName );
+        printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
+        Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+        Aig_ManStop( pNew );
     }
     else 
     {
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e6f8b8f2..f09d7626 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -199,7 +199,7 @@ struct Abc_Ntk_t_
     int *             pModel;        // counter-example (for miters)
     void *            pSeqModel;     // counter-example (for sequential miters)
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
-    void *            pManExdc;      // the EXDC network (if given)
+    void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;
     Hop_Man_t *       pHaig;         // history AIG
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index af23f18a..de517705 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -677,7 +677,7 @@ void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // collect the CI
-    if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+    if ( Abc_ObjIsCi(pNode) )//|| Abc_ObjFaninNum(pNode) == 0 )
     {
         Vec_PtrPush( vNodes, pNode );
         return;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 85cb1569..b1f75ab6 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -23,8 +23,6 @@
 #include "main.h"
 #include "mio.h"
 
-#include "aig.h"
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -348,8 +346,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-    if ( pNtk->pManExdc )
-        pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 );
+    if ( pNtk->pExcare )
+        pNtkNew->pExcare = Abc_NtkDup( pNtk->pExcare );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
     pNtk->pCopy = pNtkNew;
@@ -941,11 +939,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // free EXDC Ntk
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
-    if ( pNtk->pManExdc )
-    {
-        Aig_ManStop( pNtk->pManExdc );
-        pNtk->pManExdc = NULL;
-    }
+    if ( pNtk->pExcare )
+        Abc_NtkDelete( pNtk->pExcare );
     // dereference the BDDs
     if ( Abc_NtkHasBdd(pNtk) )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 338f38fc..266f8075 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -101,6 +101,7 @@ static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCareSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -280,6 +281,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "care_set",      Abc_CommandCareSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
@@ -3257,14 +3259,18 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    pPars->nWinTfoLevs  =  2;
-    pPars->nFanoutsMax  = 10;
-    pPars->nGrowthLevel =  0;
-    pPars->fArea        =  0;
-    pPars->fVerbose     =  0;
-    pPars->fVeryVerbose =  0;
+    pPars->nWinTfoLevs  =   2;
+    pPars->nFanoutsMax  =  10;
+    pPars->nDepthMax    =  20;
+    pPars->nDivMax      = 200;
+    pPars->nWinSizeMax  = 300;
+    pPars->nGrowthLevel =   0;
+    pPars->fResub       =   1;
+    pPars->fArea        =   0;
+    pPars->fVerbose     =   0;
+    pPars->fVeryVerbose =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3276,7 +3282,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 ) 
+            if ( pPars->nWinTfoLevs < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -3290,6 +3296,28 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFanoutsMax < 1 ) 
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nDepthMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nDepthMax < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWinSizeMax < 0 ) 
+                goto usage;
+            break;
         case 'L':
             if ( globalUtilOptind >= argc )
             {
@@ -3301,6 +3329,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) 
                 goto usage;
             break;
+        case 'r':
+            pPars->fResub ^= 1;
+            break;
         case 'a':
             pPars->fArea ^= 1;
             break;
@@ -3337,14 +3368,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" );
+    fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" );
     fprintf( pErr, "\t           performs don't-care-based optimization of logic networks\n" );
-    fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs );
-    fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax );
+    fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
+    fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
+    fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
+    fprintf( pErr, "\t-M <num> : the max size of  window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
     fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-//    fprintf( pErr, "\t-a       : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
-    fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
-//    fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-a       : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" );
+    fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
+    fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
     return 1;
 } 
@@ -5750,6 +5784,93 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandCareSet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
+    char * FileName;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pNtkNew = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+        return 1;
+    }
+
+    // replace the EXDC
+    if ( pNtk->pExcare )
+    {
+        Abc_NtkDelete( pNtk->pExcare );
+        pNtk->pExcare = NULL;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    pNtkRes->pExcare = pNtkNew;
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: care_set [-h] <file>\n" );
+    fprintf( pErr, "\t         sets the network from file as a care for the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : file with the new care network\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 2a15c3a4..72606dcf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -184,11 +184,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
             Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
         }
-    if ( pMan->pManExdc )
-    {
-        pNtkNew->pManExdc = pMan->pManExdc;
-        pMan->pManExdc = NULL;
-    }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index bb56c22c..5d24398b 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "if.h"
 #include "kit.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -87,7 +88,6 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     // duplicate EXDC
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index a7ca3819..9fc6a253 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -43,7 +43,11 @@ struct Mfs_Par_t_
     // general parameters
     int           nWinTfoLevs;   // the maximum fanout levels
     int           nFanoutsMax;   // the maximum number of fanouts
-    int           nGrowthLevel;  // the maximum allowed growth in level after one iteration of resynthesis
+    int           nDepthMax;     // the maximum number of logic levels
+    int           nDivMax;       // the maximum number of divisors
+    int           nWinSizeMax;   // the maximum size of the window
+    int           nGrowthLevel;  // the maximum allowed growth in level
+    int           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
     int           fDelay;        // performs optimization for delay
     int           fVerbose;      // enable basic stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index fe0d84c3..332a6ad9 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Core procedures of this package.]
 
   Author      [Alan Mishchenko]
   
@@ -39,9 +39,64 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    int clk;
+    p->nNodesTried++;
+    // prepare data structure for this node
+    Mfs_ManClean( p ); 
+    // compute window roots, window support, and window nodes
+clk = clock();
+    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+p->timeWin += clock() - clk;
+    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+        return 1;
+    // compute the divisors of the window
+clk = clock();
+    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+p->timeDiv += clock() - clk;
+    // construct AIG for the window
+clk = clock();
+    p->pAigWin = Abc_NtkConstructAig( p, pNode );
+p->timeAig += clock() - clk;
+    // translate it into CNF
+clk = clock();
+    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
+p->timeCnf += clock() - clk;
+    // create the SAT problem
+clk = clock();
+    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+    if ( p->pSat == NULL )
+    {
+        p->nNodesBad++;
+        return 1;
+    }
+    // solve the SAT problem
+    if ( p->pPars->fArea )
+        Abc_NtkMfsResubArea( p, pNode );
+    else
+        Abc_NtkMfsResubEdge( p, pNode );
+p->timeSat += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     int clk;
+    p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
@@ -80,9 +135,14 @@ p->timeSat += clock() - clk;
 ***********************************************************************/
 int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 {
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+
+    ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, Counter;
+    int i, clk = clock();
+    int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
+    int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
     assert( Abc_NtkIsLogic(pNtk) );
     if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
@@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         return 0;
     }
     assert( Abc_NtkHasAig(pNtk) );
-    if ( pNtk->pManExdc != NULL )
-        printf( "Performing don't-care computation with don't-cares.\n" );
 
     // start the manager
-    p = Mfs_ManAlloc();
-    p->pPars = pPars;
+    p = Mfs_ManAlloc( pPars );
     p->pNtk  = pNtk;
-    p->pCare = pNtk->pManExdc;
+    if ( pNtk->pExcare )
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+        p->pCare = Abc_NtkToDar( pTemp, 0 );
+        Abc_NtkDelete( pTemp );
+    }
+    if ( pPars->fVerbose )
+    {
+        if ( p->pCare != NULL )
+            printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+        else
+            printf( "Performing optimization without constraints.\n" );
+    }
+    if ( !pPars->fResub )
+        printf( "Currently don't-cares are not used but the stats are printed.\n" );
 
     // label the register outputs
     if ( p->pCare )
     {
-        Counter = 1;
         Abc_NtkForEachCi( pNtk, pObj, i )
-            if ( Abc_ObjFaninNum(pObj) == 0 )
-                pObj->pData = NULL;
-            else
-                pObj->pData = (void *)Counter++;
-        assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
+            pObj->pData = (void *)i;
     }
+ 
+    // compute levels
+    Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // compute don't-cares for each node
+    p->nTotalNodesBeg = nTotalNodesBeg;
+    p->nTotalEdgesBeg = nTotalEdgesBeg;
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pObj, i )
-        Abc_NtkMfsNode( p, pObj );
+    {
+        if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+            continue;
+        if ( !p->pPars->fVeryVerbose )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( pPars->fResub )
+            Abc_NtkMfsResub( p, pObj );
+        else
+            Abc_NtkMfsNode( p, pObj );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkStopReverseLevels( pNtk );
+    p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
+    p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
 
     // undo labesl
     if ( p->pCare )
@@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     }
 
     // free the manager
+    p->timeTotal = clock() - clk;
     Mfs_ManStop( p );
     return 1;
 }
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
new file mode 100644
index 00000000..7b156b97
--- /dev/null
+++ b/src/opt/mfs/mfsDiv.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+  FileName    [mfsDiv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to compute candidate divisors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsWinMarkTfi_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    if ( Abc_ObjIsCi(pObj) )
+    {
+        Vec_PtrPush( vCone, pObj );
+        return;
+    }
+    assert( Abc_ObjIsNode(pObj) );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Abc_MfsWinMarkTfi_rec( pFanin, vCone );
+    Vec_PtrPush( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsWinMarkTfi( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vCone;
+    vCone = Vec_PtrAlloc( 100 );
+    Abc_MfsWinMarkTfi_rec( pNode, vCone );
+    return vCone;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_MfsWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsNodeDeref_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        assert( pFanin->vFanouts.nSize > 0 );
+        if ( --pFanin->vFanouts.nSize == 0 )
+            Counter += Abc_MfsNodeDeref_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsNodeRef_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin->vFanouts.nSize++ == 0 )
+            Counter += Abc_MfsNodeRef_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels MFFC of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsWinVisitMffc( Abc_Obj_t * pNode )
+{
+    int Count1, Count2;
+    assert( Abc_ObjIsNode(pNode) );
+    // dereference the node (mark with the current trav ID)
+    Count1 = Abc_MfsNodeDeref_rec( pNode );
+    // reference it back
+    Count2 = Abc_MfsNodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes divisors and add them to nodes in the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax )
+{
+    Vec_Ptr_t * vCone, * vDivs;
+    Abc_Obj_t * pObj, * pFanout, * pFanin;
+    int k, f, m;
+    int nDivsPlus = 0, nTrueSupp;
+    assert( p->vDivs == NULL );
+
+    // mark the TFI with the current trav ID
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    vCone = Abc_MfsWinMarkTfi( pNode );
+
+    // count the number of PIs
+    nTrueSupp = 0;
+    Vec_PtrForEachEntry( vCone, pObj, k )
+        nTrueSupp += Abc_ObjIsCi(pObj);
+//    printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
+
+    // mark with the current trav ID those nodes that should not be divisors:
+    // (1) the node and its TFO
+    // (2) the MFFC of the node
+    // (3) the node's fanins (these are treated as a special case)
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
+    Abc_MfsWinVisitMffc( pNode );
+    Abc_ObjForEachFanin( pNode, pObj, k )
+        Abc_NodeSetTravIdCurrent( pObj );
+
+    // at this point the nodes are marked with two trav IDs:
+    // nodes to be collected as divisors are marked with previous trav ID
+    // nodes to be avoided as divisors are marked with current trav ID
+
+    // start collecting the divisors
+    vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+    Vec_PtrForEachEntry( vCone, pObj, k )
+    {
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > nLevDivMax )
+            continue;
+        Vec_PtrPush( vDivs, pObj );
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+    Vec_PtrFree( vCone );
+
+    // explore the fanouts of already collected divisors
+    if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+    Vec_PtrForEachEntry( vDivs, pObj, k )
+    {
+        // consider fanouts of this node
+        Abc_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // stop if there are too many fanouts
+            if ( f > 20 )
+                break;
+            // skip nodes that are already added
+            if ( Abc_NodeIsTravIdPrevious(pFanout) )
+                continue;
+            // skip nodes in the TFO or in the MFFC of node
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level >= nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not divisors
+            Abc_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
+                    break;
+            if ( m < Abc_ObjFaninNum(pFanout) )
+                continue;
+            // make sure this divisor in not among the nodes
+//            Vec_PtrForEachEntry( p->vNodes, pFanin, m )
+//                assert( pFanout != pFanin );
+            // add the node to the divisors
+            Vec_PtrPush( vDivs, pFanout );
+//            Vec_PtrPush( p->vNodes, pFanout );
+            Vec_PtrPushUnique( p->vNodes, pFanout );
+            Abc_NodeSetTravIdPrevious( pFanout );
+            nDivsPlus++;
+            if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+                break;
+        }
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+
+    // sort the divisors by level in the increasing order
+    Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease );
+
+    // add the fanins of the node
+    Abc_ObjForEachFanin( pNode, pFanin, k )
+        Vec_PtrPush( vDivs, pFanin );
+
+/*
+    printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
+    Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
+        printf( "%d ", Abc_ObjLevel(pObj) );
+    printf( "\n" );
+*/
+//printf( "%d ", p->nDivsPlus );
+//    printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), 
+//        nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
+    return vDivs;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 6ba5903e..54826bc1 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -34,6 +34,7 @@ extern "C" {
 #include "aig.h"
 #include "cnf.h"
 #include "satSolver.h"
+#include "satStore.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -52,11 +53,23 @@ struct Mfs_Man_t_
     Vec_Ptr_t *         vRoots;    // the roots of the window
     Vec_Ptr_t *         vSupp;     // the support of the window
     Vec_Ptr_t *         vNodes;    // the internal nodes of the window
+    Vec_Ptr_t *         vDivs;     // the divisors of the node
+    Vec_Int_t *         vDivLits;  // the SAT literals of divisor nodes
     Vec_Int_t *         vProjVars; // the projection variables
+    // intermediate simulation data
+    Vec_Ptr_t *         vDivCexes; // the counter-example for dividors
+    int                 nDivWords; // the number of words
+    int                 nCexes;    // the numbe rof current counter-examples
+    int                 nSatCalls; 
+    int                 nSatCexes;
     // solving data
     Aig_Man_t *         pAigWin;   // window AIG with constraints
     Cnf_Dat_t *         pCnf;      // the CNF for the window
     sat_solver *        pSat;      // the SAT solver used 
+    Int_Man_t *         pMan;      // interpolation manager;
+    Vec_Int_t *         vMem;      // memory for intermediate SOPs
+    Vec_Vec_t *         vLevels;   // levelized structure for updating
+    Vec_Ptr_t *         vFanins;   // the new set of fanins
     // the result of solving
     int                 nFanins;   // the number of fanins
     int                 nWords;    // the number of words
@@ -64,14 +77,24 @@ struct Mfs_Man_t_
     unsigned            uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)];  // the computed care-set
     // performance statistics
     int                 nNodesTried;
-    int                 nNodesBad;
+    int                 nNodesResub;
+    int                 nNodesGained;
     int                 nMintsCare;
     int                 nMintsTotal;
+    int                 nNodesBad;
+    // node/edge stats
+    int                 nTotalNodesBeg;
+    int                 nTotalNodesEnd;
+    int                 nTotalEdgesBeg;
+    int                 nTotalEdgesEnd;
     // statistics
     int                 timeWin;
+    int                 timeDiv;
     int                 timeAig;
     int                 timeCnf;
     int                 timeSat;
+    int                 timeInt;
+    int                 timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -86,10 +109,18 @@ struct Mfs_Man_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== mfsDiv.c ==========================================================*/
+extern Vec_Ptr_t *      Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
+/*=== mfsInter.c ==========================================================*/
+extern sat_solver *     Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
+extern Hop_Obj_t *      Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
 /*=== mfsMan.c ==========================================================*/
-extern Mfs_Man_t *      Mfs_ManAlloc();
+extern Mfs_Man_t *      Mfs_ManAlloc( Mfs_Par_t * pPars );
 extern void             Mfs_ManStop( Mfs_Man_t * p );
 extern void             Mfs_ManClean( Mfs_Man_t * p );
+/*=== mfsResub.c ==========================================================*/
+extern int              Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
 extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
new file mode 100644
index 00000000..16db5061
--- /dev/null
+++ b/src/opt/mfs/mfsInter.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [mfsInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures for computing resub function by interpolation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constraints for the two-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
+{
+    lit Lits[3];
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates miter for checking resubsitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    sat_solver * pSat;
+    Aig_Obj_t * pObjPo;
+    int Lits[2], status, iVar, i, c;
+
+    // get the literal for the output of F
+    pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
+    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
+
+    // collect the outputs of the divisors
+    Vec_IntClear( p->vProjVars );
+    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
+    {
+        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+    }
+    assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
+    if ( pCands )
+        sat_solver_store_alloc( pSat );
+
+    // load the first copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // add the clause for the first output of F
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    // bookmark the clauses of A
+    if ( pCands )
+        sat_solver_store_mark_clauses_a( pSat );
+
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
+    // load the second copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
+    // add the clause for the second output of F
+    Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    if ( pCands )
+    {
+        // add relevant clauses for EXOR gates
+        for ( c = 0; c < nCands; c++ )
+        {
+            // get the variable number of this divisor
+            i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+            // get the corresponding SAT variable
+            iVar = Vec_IntEntry( p->vProjVars, i );
+            // add the corresponding EXOR gate
+            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            // add the corresponding clause
+            if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+        }
+        // bookmark the roots
+        sat_solver_store_mark_roots( pSat );
+    }
+    else
+    {
+        // add the clauses for the EXOR gates - and remember their outputs
+        Vec_IntForEachEntry( p->vProjVars, iVar, i )
+        {
+            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+        }
+        // simplify the solver
+        status = sat_solver_simplify(pSat);
+        if ( status == 0 )
+        {
+//            printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
+    sat_solver * pSat;
+    Sto_Man_t * pCnf = NULL;
+    unsigned * puTruth;
+    Kit_Graph_t * pGraph;
+    Hop_Obj_t * pFunc;
+    int nFanins, status;
+
+    // derive the SAT solver for interpolation
+    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status != l_False )
+    {
+        printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
+        return NULL;
+    }
+    // get the learned clauses
+    pCnf = sat_solver_store_release( pSat );
+    sat_solver_delete( pSat );
+
+    // derive the interpolant
+    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+    Sto_ManFree( pCnf );
+    assert( nFanins == nCands );
+
+    // transform interpolant into AIG
+    pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+    pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph );
+    Kit_GraphFree( pGraph );
+    return pFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 1341e373..67981d5a 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    [Procedure to manipulation the manager.]
+  Synopsis    [Procedures working with the manager.]
 
   Author      [Alan Mishchenko]
   
@@ -28,7 +28,6 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -40,13 +39,21 @@
   SeeAlso     []
 
 ***********************************************************************/
-Mfs_Man_t * Mfs_ManAlloc()
+Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
 {
     Mfs_Man_t * p;
     // start the manager
     p = ALLOC( Mfs_Man_t, 1 );
     memset( p, 0, sizeof(Mfs_Man_t) );
+    p->pPars     = pPars;
     p->vProjVars = Vec_IntAlloc( 100 );
+    p->vDivLits  = Vec_IntAlloc( 100 );
+    p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
+    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
+    p->pMan      = Int_ManAlloc();
+    p->vMem      = Vec_IntAlloc( 0 );
+    p->vLevels   = Vec_VecStart( 32 );
+    p->vFanins   = Vec_PtrAlloc( 32 );
     return p;
 }
 
@@ -75,12 +82,15 @@ void Mfs_ManClean( Mfs_Man_t * p )
         Vec_PtrFree( p->vSupp );
     if ( p->vNodes )
         Vec_PtrFree( p->vNodes );
+    if ( p->vDivs )
+        Vec_PtrFree( p->vDivs );
     p->pAigWin = NULL;
-    p->pCnf = NULL;
-    p->pSat = NULL;
+    p->pCnf   = NULL;
+    p->pSat   = NULL;
     p->vRoots = NULL;
-    p->vSupp = NULL;
+    p->vSupp  = NULL;
     p->vNodes = NULL;
+    p->vDivs  = NULL;
 }
 
 /**Function*************************************************************
@@ -96,14 +106,31 @@ void Mfs_ManClean( Mfs_Man_t * p )
 ***********************************************************************/
 void Mfs_ManPrint( Mfs_Man_t * p )
 {
-    printf( "Nodes tried = %d. Bad nodes = %d.\n", 
-        p->nNodesTried, p->nNodesBad );
-    printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n", 
-        p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal );
-    PRT( "Win", p->timeWin );
-    PRT( "Aig", p->timeAig );
-    PRT( "Cnf", p->timeCnf );
-    PRT( "Sat", p->timeSat );
+    if ( p->pPars->fResub )
+    {
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nTotalNodesBeg-p->nTotalNodesEnd, 
+            100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
+            100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+        printf( "\n" );
+        printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+    }
+    else
+    {
+        printf( "Nodes = %d.  Care mints = %d. Total mints = %d. Ratio = %5.2f.\n", 
+            p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal );
+    }
+    PRTP( "Win", p->timeWin            ,  p->timeTotal );
+    PRTP( "Div", p->timeDiv            ,  p->timeTotal );
+    PRTP( "Aig", p->timeAig            ,  p->timeTotal );
+    PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
+    PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
+    PRTP( "Int", p->timeInt            ,  p->timeTotal );
+    PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
+
 }
 
 /**Function*************************************************************
@@ -119,9 +146,18 @@ void Mfs_ManPrint( Mfs_Man_t * p )
 ***********************************************************************/
 void Mfs_ManStop( Mfs_Man_t * p )
 {
-    Mfs_ManPrint( p );
+    if ( p->pPars->fVerbose )
+        Mfs_ManPrint( p );
+    if ( p->pCare )
+        Aig_ManStop( p->pCare );
     Mfs_ManClean( p );
+    Int_ManFree( p->pMan );
+    Vec_IntFree( p->vMem );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vFanins );
     Vec_IntFree( p->vProjVars );
+    Vec_IntFree( p->vDivLits );
+    Vec_PtrFree( p->vDivCexes );
     free( p );
 }
 
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
new file mode 100644
index 00000000..ae1132f2
--- /dev/null
+++ b/src/opt/mfs/mfsResub.c
@@ -0,0 +1,276 @@
+/**CFile****************************************************************
+
+  FileName    [mfsResub.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to perform resubstitution.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the network after resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+{
+    Abc_Obj_t * pObjNew, * pFanin;
+    int k;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
+    // update the level of the node
+    Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tries resubstitution.]
+
+  Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    unsigned * pData, * pDataTot;
+    int RetValue, iVar, i;
+    p->nSatCalls++;
+    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_False || RetValue == l_True );
+    if ( RetValue == l_False )
+        return 1;
+    p->nSatCexes++;
+    // store the counter-example
+    pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
+    assert( pData[0] == 0 );
+    Vec_IntForEachEntry( p->vProjVars, iVar, i )
+    {
+        if ( sat_solver_var_value( p->pSat, iVar ) )
+            Aig_InfoSetBit( pData, i );
+    }
+    // AND the result with the previous ones
+    pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+    for ( i = 0; i < p->nDivWords; i++ )
+        pDataTot[i] &= pData[i];
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+{
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData;
+    int pCands[MFS_FANIN_MAX];
+    int iVar, i, nCands, clk;
+    Abc_Obj_t * pFanin;
+    Hop_Obj_t * pFunc;
+    assert( iFanin >= 0 );
+
+    // clean simulation info
+    Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); 
+    pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+    memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+    p->nCexes = 0;
+
+    if ( fVeryVerbose )
+    {
+        printf( "\n" );
+        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanin = %d (out of %d). MFFC = %d\n", 
+            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
+            iFanin, Abc_ObjFaninNum(pNode), 
+            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( i == iFanin )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    {
+        if ( fVeryVerbose )
+        printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
+        p->nNodesResub++;
+//        p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+        // derive the function
+        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        // update the network
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+        return 1;
+    }
+
+    if ( fOnlyRemove )
+        return 0;
+
+    // shift variables by 1
+    for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+        p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+    p->vFanins->nSize++;
+
+    if ( fVeryVerbose )
+    {
+        for ( i = 0; i < 8; i++ )
+            printf( " " );
+        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+            if ( i == iFanin )
+                printf( "*" );
+            else
+                printf( "%c", 'a' + i );
+        printf( "\n" );
+    }
+    iVar = -1;
+    while ( 1 )
+    {
+        if ( fVeryVerbose )
+        {
+            printf( "%3d: %2d ", p->nCexes, iVar );
+            pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
+//            Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
+            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
+                printf( "%d", Aig_InfoHasBit(pData, i) );
+            printf( "\n" );
+        }
+
+        // find the next divisor to try
+        pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+        for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
+            if ( Aig_InfoHasBit( pData, iVar ) )
+                break;
+        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
+            return 0;
+        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
+        {
+            if ( fVeryVerbose )
+            printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
+            p->nNodesResub++;
+//            p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+            // derive the function
+            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
+            // update the network
+//            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+                return 1;
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+                return 1;
+        }
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
+                return 1;
+        }
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index d995000f..efb09b39 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Procedures to compute don't-cares using SAT.]
 
   Author      [Alan Mishchenko]
   
@@ -43,9 +43,11 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
 {
     int Lits[MFS_FANIN_MAX];
     int RetValue, iVar, b, Mint;
-    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
-    if ( RetValue != l_True )
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_False || RetValue == l_True );
+    if ( RetValue == l_False )
         return 0;
+    p->nCares++;
     // add SAT assignment to the solver
     Mint = 0;
     Vec_IntForEachEntry( p->vProjVars, iVar, b )
@@ -95,15 +97,19 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
     memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
 
     // iterate through the SAT assignments
-    while ( Abc_NtkMfsSolveSat_iter( p ) );
-
-    // write statistics
     p->nCares = 0;
-    for ( i = 0; i < p->nWords; i++ )
-        p->nCares += Aig_WordCountOnes( p->uCare[i] );
+    while ( Abc_NtkMfsSolveSat_iter(p) );
 
+    // write statistics
     p->nMintsCare  += p->nCares;
-    p->nMintsTotal += 32 * p->nWords;
+    p->nMintsTotal += (1<<p->nFanins);
+
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "Node %4d : Care = %2d. Total = %2d.  ", pNode->Id, p->nCares, (1<<p->nFanins) );
+        Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
+        printf( "\n" );
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 7b467936..8e945045 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -144,18 +144,18 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
+Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan )
 {
     Aig_Obj_t * pObj0, * pObj1;
-    if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
+    if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
         return pObj->pData;
-    Aig_ObjSetTravIdCurrent( pMan, pObj );
+    Aig_ObjSetTravIdCurrent( pCare, pObj );
     if ( Aig_ObjIsPi(pObj) )
         return pObj->pData = NULL;
-    pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
+    pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
     if ( pObj0 == NULL )
         return pObj->pData = NULL;
-    pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
+    pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
     if ( pObj1 == NULL )
         return pObj->pData = NULL;
     pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
@@ -184,6 +184,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
     pMan = Aig_ManStart( 1000 );
     // construct the root node's AIG cone
     pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
+//    assert( Aig_ManConst1(pMan) == pObjAig );
     Aig_ObjCreatePo( pMan, pObjAig );
     if ( p->pCare )
     {
@@ -191,27 +192,43 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
         Aig_ManIncrementTravId( p->pCare );
         Vec_PtrForEachEntry( p->vSupp, pFanin, i )
         {
-            if ( pFanin->pData == NULL )
-                continue;
-            pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
+            pPi = Aig_ManPi( p->pCare, (int)pFanin->pData );
             Aig_ObjSetTravIdCurrent( p->pCare, pPi );
             pPi->pData = pFanin->pCopy;
         }
         // construct the constraints
         Aig_ManForEachPo( p->pCare, pPo, i )
         {
-            pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan );
+//            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                continue;
+            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
             if ( pObjAig == NULL )
                 continue;
             pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
             Aig_ObjCreatePo( pMan, pObjAig );
         }
     }
-    // construct the fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
+    if ( p->pPars->fResub )
     {
-        pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+        // construct the node
+        pObjAig = (Aig_Obj_t *)pNode->pCopy;
         Aig_ObjCreatePo( pMan, pObjAig );
+        // construct the divisors
+        Vec_PtrForEachEntry( p->vDivs, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+    }
+    else
+    {
+        // construct the fanins
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
     }
     Aig_ManCleanup( pMan );
     return pMan;
diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c
index b812d44d..e3e5e24e 100644
--- a/src/opt/mfs/mfsWin.c
+++ b/src/opt/mfs/mfsWin.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Procedures to compute windows stretching to the PIs.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
index 7b9f1260..544accec 100644
--- a/src/opt/mfs/module.make
+++ b/src/opt/mfs/module.make
@@ -1,5 +1,8 @@
 SRC +=  src/opt/mfs/mfsCore.c \
+    src/opt/mfs/mfsDiv.c \
+    src/opt/mfs/mfsInter.c \
     src/opt/mfs/mfsMan.c \
+    src/opt/mfs/mfsResub.c \
     src/opt/mfs/mfsSat.c \
     src/opt/mfs/mfsStrash.c \
     src/opt/mfs/mfsWin.c
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index cb448fc0..a19a1573 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -183,12 +183,15 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
 {
     Abc_Obj_t * pObjNew, * pFanin;
     int k;
+
     // create the new node
     pObjNew = Abc_NtkCreateNode( pObj->pNtk );
     pObjNew->pData = pFunc;
     Vec_PtrForEachEntry( vFanins, pFanin, k )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
+//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
     // update the level of the node
     Abc_NtkUpdate( pObj, pObjNew, vLevels );
 }
author	Alan Mishchenko <alanmi@berkeley.edu>	2008-02-05 08:01:00 -0800
committer	Alan Mishchenko <alanmi@berkeley.edu>	2008-02-05 08:01:00 -0800
commit	7174787abafe80437892b55a53f994da85a37342 (patch)
tree	0df4c6f35d99111d757aa9b8091853b8f88ee762
parent	3b790eb17e54cd922440a1a3b18a5cfdd5cbcadb (diff)
download	abc-7174787abafe80437892b55a53f994da85a37342.tar.gz abc-7174787abafe80437892b55a53f994da85a37342.tar.bz2 abc-7174787abafe80437892b55a53f994da85a37342.zip