Version abc51225

25 files changed, 2564 insertions, 111 deletions

diff --git a/abc.opt b/abc.opt
index c61b856d..b6e9637f 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index 08975441..17867ca9 100644
--- a/abc.plg
+++ b/abc.plg
@@ -3,9 +3,678 @@
 <pre>
 <h1>Build Log</h1>
 <h3>
---------------------Configuration: abc - Win32 Release--------------------
+--------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" with contents
+[
+/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
+"C:\_projects\abc\src\opt\xyz\xyzCore.c"
+]
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14F9.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.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 /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
+.\Debug\abcAig.obj
+.\Debug\abcCheck.obj
+.\Debug\abcDfs.obj
+.\Debug\abcFanio.obj
+.\Debug\abcFunc.obj
+.\Debug\abcLatch.obj
+.\Debug\abcMinBase.obj
+.\Debug\abcNames.obj
+.\Debug\abcNetlist.obj
+.\Debug\abcNtk.obj
+.\Debug\abcObj.obj
+.\Debug\abcRefs.obj
+.\Debug\abcShow.obj
+.\Debug\abcSop.obj
+.\Debug\abcUtil.obj
+.\Debug\abc.obj
+.\Debug\abcAttach.obj
+.\Debug\abcBalance.obj
+.\Debug\abcCollapse.obj
+.\Debug\abcCut.obj
+.\Debug\abcDsd.obj
+.\Debug\abcFpga.obj
+.\Debug\abcFraig.obj
+.\Debug\abcFxu.obj
+.\Debug\abcMap.obj
+.\Debug\abcMiter.obj
+.\Debug\abcNtbdd.obj
+.\Debug\abcPga.obj
+.\Debug\abcPrint.obj
+.\Debug\abcReconv.obj
+.\Debug\abcRefactor.obj
+.\Debug\abcRenode.obj
+.\Debug\abcRewrite.obj
+.\Debug\abcSat.obj
+.\Debug\abcStrash.obj
+.\Debug\abcSweep.obj
+.\Debug\abcSymm.obj
+.\Debug\abcTiming.obj
+.\Debug\abcUnreach.obj
+.\Debug\abcVanEijk.obj
+.\Debug\abcVanImp.obj
+.\Debug\abcVerify.obj
+.\Debug\seqAigCore.obj
+.\Debug\seqAigIter.obj
+.\Debug\seqCreate.obj
+.\Debug\seqFpgaCore.obj
+.\Debug\seqFpgaIter.obj
+.\Debug\seqLatch.obj
+.\Debug\seqMan.obj
+.\Debug\seqMapCore.obj
+.\Debug\seqMapIter.obj
+.\Debug\seqRetCore.obj
+.\Debug\seqRetIter.obj
+.\Debug\seqShare.obj
+.\Debug\seqUtil.obj
+.\Debug\cmd.obj
+.\Debug\cmdAlias.obj
+.\Debug\cmdApi.obj
+.\Debug\cmdFlag.obj
+.\Debug\cmdHist.obj
+.\Debug\cmdUtils.obj
+.\Debug\io.obj
+.\Debug\ioRead.obj
+.\Debug\ioReadBaf.obj
+.\Debug\ioReadBench.obj
+.\Debug\ioReadBlif.obj
+.\Debug\ioReadEdif.obj
+.\Debug\ioReadEqn.obj
+.\Debug\ioReadPla.obj
+.\Debug\ioReadVerilog.obj
+.\Debug\ioUtil.obj
+.\Debug\ioWriteBaf.obj
+.\Debug\ioWriteBench.obj
+.\Debug\ioWriteBlif.obj
+.\Debug\ioWriteCnf.obj
+.\Debug\ioWriteDot.obj
+.\Debug\ioWriteEqn.obj
+.\Debug\ioWriteGml.obj
+.\Debug\ioWriteList.obj
+.\Debug\ioWritePla.obj
+.\Debug\ioWriteVerilog.obj
+.\Debug\libSupport.obj
+.\Debug\main.obj
+.\Debug\mainFrame.obj
+.\Debug\mainInit.obj
+.\Debug\mainUtils.obj
+.\Debug\cuddAddAbs.obj
+.\Debug\cuddAddApply.obj
+.\Debug\cuddAddFind.obj
+.\Debug\cuddAddInv.obj
+.\Debug\cuddAddIte.obj
+.\Debug\cuddAddNeg.obj
+.\Debug\cuddAddWalsh.obj
+.\Debug\cuddAndAbs.obj
+.\Debug\cuddAnneal.obj
+.\Debug\cuddApa.obj
+.\Debug\cuddAPI.obj
+.\Debug\cuddApprox.obj
+.\Debug\cuddBddAbs.obj
+.\Debug\cuddBddCorr.obj
+.\Debug\cuddBddIte.obj
+.\Debug\cuddBridge.obj
+.\Debug\cuddCache.obj
+.\Debug\cuddCheck.obj
+.\Debug\cuddClip.obj
+.\Debug\cuddCof.obj
+.\Debug\cuddCompose.obj
+.\Debug\cuddDecomp.obj
+.\Debug\cuddEssent.obj
+.\Debug\cuddExact.obj
+.\Debug\cuddExport.obj
+.\Debug\cuddGenCof.obj
+.\Debug\cuddGenetic.obj
+.\Debug\cuddGroup.obj
+.\Debug\cuddHarwell.obj
+.\Debug\cuddInit.obj
+.\Debug\cuddInteract.obj
+.\Debug\cuddLCache.obj
+.\Debug\cuddLevelQ.obj
+.\Debug\cuddLinear.obj
+.\Debug\cuddLiteral.obj
+.\Debug\cuddMatMult.obj
+.\Debug\cuddPriority.obj
+.\Debug\cuddRead.obj
+.\Debug\cuddRef.obj
+.\Debug\cuddReorder.obj
+.\Debug\cuddSat.obj
+.\Debug\cuddSign.obj
+.\Debug\cuddSolve.obj
+.\Debug\cuddSplit.obj
+.\Debug\cuddSubsetHB.obj
+.\Debug\cuddSubsetSP.obj
+.\Debug\cuddSymmetry.obj
+.\Debug\cuddTable.obj
+.\Debug\cuddUtil.obj
+.\Debug\cuddWindow.obj
+.\Debug\cuddZddCount.obj
+.\Debug\cuddZddFuncs.obj
+.\Debug\cuddZddGroup.obj
+.\Debug\cuddZddIsop.obj
+.\Debug\cuddZddLin.obj
+.\Debug\cuddZddMisc.obj
+.\Debug\cuddZddPort.obj
+.\Debug\cuddZddReord.obj
+.\Debug\cuddZddSetop.obj
+.\Debug\cuddZddSymm.obj
+.\Debug\cuddZddUtil.obj
+.\Debug\epd.obj
+.\Debug\mtrBasic.obj
+.\Debug\mtrGroup.obj
+.\Debug\parseCore.obj
+.\Debug\parseStack.obj
+.\Debug\dsdApi.obj
+.\Debug\dsdCheck.obj
+.\Debug\dsdLocal.obj
+.\Debug\dsdMan.obj
+.\Debug\dsdProc.obj
+.\Debug\dsdTree.obj
+.\Debug\reoApi.obj
+.\Debug\reoCore.obj
+.\Debug\reoProfile.obj
+.\Debug\reoSift.obj
+.\Debug\reoSwap.obj
+.\Debug\reoTest.obj
+.\Debug\reoTransfer.obj
+.\Debug\reoUnits.obj
+.\Debug\added.obj
+.\Debug\solver.obj
+.\Debug\msatActivity.obj
+.\Debug\msatClause.obj
+.\Debug\msatClauseVec.obj
+.\Debug\msatMem.obj
+.\Debug\msatQueue.obj
+.\Debug\msatRead.obj
+.\Debug\msatSolverApi.obj
+.\Debug\msatSolverCore.obj
+.\Debug\msatSolverIo.obj
+.\Debug\msatSolverSearch.obj
+.\Debug\msatSort.obj
+.\Debug\msatVec.obj
+.\Debug\fraigApi.obj
+.\Debug\fraigCanon.obj
+.\Debug\fraigFanout.obj
+.\Debug\fraigFeed.obj
+.\Debug\fraigMan.obj
+.\Debug\fraigMem.obj
+.\Debug\fraigNode.obj
+.\Debug\fraigPrime.obj
+.\Debug\fraigSat.obj
+.\Debug\fraigTable.obj
+.\Debug\fraigUtil.obj
+.\Debug\fraigVec.obj
+.\Debug\csat_apis.obj
+.\Debug\fxu.obj
+.\Debug\fxuCreate.obj
+.\Debug\fxuHeapD.obj
+.\Debug\fxuHeapS.obj
+.\Debug\fxuList.obj
+.\Debug\fxuMatrix.obj
+.\Debug\fxuPair.obj
+.\Debug\fxuPrint.obj
+.\Debug\fxuReduce.obj
+.\Debug\fxuSelect.obj
+.\Debug\fxuSingle.obj
+.\Debug\fxuUpdate.obj
+.\Debug\rwrDec.obj
+.\Debug\rwrEva.obj
+.\Debug\rwrExp.obj
+.\Debug\rwrLib.obj
+.\Debug\rwrMan.obj
+.\Debug\rwrPrint.obj
+.\Debug\rwrUtil.obj
+.\Debug\cutApi.obj
+.\Debug\cutCut.obj
+.\Debug\cutMan.obj
+.\Debug\cutMerge.obj
+.\Debug\cutNode.obj
+.\Debug\cutOracle.obj
+.\Debug\cutSeq.obj
+.\Debug\cutTruth.obj
+.\Debug\decAbc.obj
+.\Debug\decFactor.obj
+.\Debug\decMan.obj
+.\Debug\decPrint.obj
+.\Debug\decUtil.obj
+.\Debug\simMan.obj
+.\Debug\simSat.obj
+.\Debug\simSeq.obj
+.\Debug\simSupp.obj
+.\Debug\simSwitch.obj
+.\Debug\simSym.obj
+.\Debug\simSymSat.obj
+.\Debug\simSymSim.obj
+.\Debug\simSymStr.obj
+.\Debug\simUtils.obj
+.\Debug\xyzBuild.obj
+.\Debug\xyzCore.obj
+.\Debug\xyzMan.obj
+.\Debug\xyzMinEsop.obj
+.\Debug\xyzMinMan.obj
+.\Debug\xyzMinSop.obj
+.\Debug\xyzMinUtil.obj
+.\Debug\xyzTest.obj
+.\Debug\fpga.obj
+.\Debug\fpgaCore.obj
+.\Debug\fpgaCreate.obj
+.\Debug\fpgaCut.obj
+.\Debug\fpgaCutUtils.obj
+.\Debug\fpgaFanout.obj
+.\Debug\fpgaLib.obj
+.\Debug\fpgaMatch.obj
+.\Debug\fpgaSwitch.obj
+.\Debug\fpgaTime.obj
+.\Debug\fpgaTruth.obj
+.\Debug\fpgaUtils.obj
+.\Debug\fpgaVec.obj
+.\Debug\mapper.obj
+.\Debug\mapperCanon.obj
+.\Debug\mapperCore.obj
+.\Debug\mapperCreate.obj
+.\Debug\mapperCut.obj
+.\Debug\mapperCutUtils.obj
+.\Debug\mapperFanout.obj
+.\Debug\mapperLib.obj
+.\Debug\mapperMatch.obj
+.\Debug\mapperRefs.obj
+.\Debug\mapperSuper.obj
+.\Debug\mapperSwitch.obj
+.\Debug\mapperTable.obj
+.\Debug\mapperTime.obj
+.\Debug\mapperTree.obj
+.\Debug\mapperTruth.obj
+.\Debug\mapperUtils.obj
+.\Debug\mapperVec.obj
+.\Debug\mio.obj
+.\Debug\mioApi.obj
+.\Debug\mioFunc.obj
+.\Debug\mioRead.obj
+.\Debug\mioUtils.obj
+.\Debug\super.obj
+.\Debug\superAnd.obj
+.\Debug\superGate.obj
+.\Debug\superWrite.obj
+.\Debug\pgaCore.obj
+.\Debug\pgaMan.obj
+.\Debug\pgaMatch.obj
+.\Debug\pgaUtil.obj
+.\Debug\extraBddKmap.obj
+.\Debug\extraBddMisc.obj
+.\Debug\extraBddSymm.obj
+.\Debug\extraUtilBitMatrix.obj
+.\Debug\extraUtilCanon.obj
+.\Debug\extraUtilFile.obj
+.\Debug\extraUtilMemory.obj
+.\Debug\extraUtilMisc.obj
+.\Debug\extraUtilProgress.obj
+.\Debug\extraUtilReader.obj
+.\Debug\st.obj
+.\Debug\stmm.obj
+.\Debug\cpu_stats.obj
+.\Debug\cpu_time.obj
+.\Debug\datalimit.obj
+.\Debug\getopt.obj
+.\Debug\pathsearch.obj
+.\Debug\safe_mem.obj
+.\Debug\strsav.obj
+.\Debug\texpand.obj
+.\Debug\mvc.obj
+.\Debug\mvcApi.obj
+.\Debug\mvcCompare.obj
+.\Debug\mvcContain.obj
+.\Debug\mvcCover.obj
+.\Debug\mvcCube.obj
+.\Debug\mvcDivide.obj
+.\Debug\mvcDivisor.obj
+.\Debug\mvcList.obj
+.\Debug\mvcLits.obj
+.\Debug\mvcMan.obj
+.\Debug\mvcOpAlg.obj
+.\Debug\mvcOpBool.obj
+.\Debug\mvcPrint.obj
+.\Debug\mvcSort.obj
+.\Debug\mvcUtils.obj
+.\Debug\msatOrderJ.obj
+]
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FA.tmp"
+<h3>Output Window</h3>
+Compiling...
+xyzCore.c
+Linking...
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp" with contents
+[
+/nologo /o"Debug/abc.bsc" 
+.\Debug\abcAig.sbr
+.\Debug\abcCheck.sbr
+.\Debug\abcDfs.sbr
+.\Debug\abcFanio.sbr
+.\Debug\abcFunc.sbr
+.\Debug\abcLatch.sbr
+.\Debug\abcMinBase.sbr
+.\Debug\abcNames.sbr
+.\Debug\abcNetlist.sbr
+.\Debug\abcNtk.sbr
+.\Debug\abcObj.sbr
+.\Debug\abcRefs.sbr
+.\Debug\abcShow.sbr
+.\Debug\abcSop.sbr
+.\Debug\abcUtil.sbr
+.\Debug\abc.sbr
+.\Debug\abcAttach.sbr
+.\Debug\abcBalance.sbr
+.\Debug\abcCollapse.sbr
+.\Debug\abcCut.sbr
+.\Debug\abcDsd.sbr
+.\Debug\abcFpga.sbr
+.\Debug\abcFraig.sbr
+.\Debug\abcFxu.sbr
+.\Debug\abcMap.sbr
+.\Debug\abcMiter.sbr
+.\Debug\abcNtbdd.sbr
+.\Debug\abcPga.sbr
+.\Debug\abcPrint.sbr
+.\Debug\abcReconv.sbr
+.\Debug\abcRefactor.sbr
+.\Debug\abcRenode.sbr
+.\Debug\abcRewrite.sbr
+.\Debug\abcSat.sbr
+.\Debug\abcStrash.sbr
+.\Debug\abcSweep.sbr
+.\Debug\abcSymm.sbr
+.\Debug\abcTiming.sbr
+.\Debug\abcUnreach.sbr
+.\Debug\abcVanEijk.sbr
+.\Debug\abcVanImp.sbr
+.\Debug\abcVerify.sbr
+.\Debug\seqAigCore.sbr
+.\Debug\seqAigIter.sbr
+.\Debug\seqCreate.sbr
+.\Debug\seqFpgaCore.sbr
+.\Debug\seqFpgaIter.sbr
+.\Debug\seqLatch.sbr
+.\Debug\seqMan.sbr
+.\Debug\seqMapCore.sbr
+.\Debug\seqMapIter.sbr
+.\Debug\seqRetCore.sbr
+.\Debug\seqRetIter.sbr
+.\Debug\seqShare.sbr
+.\Debug\seqUtil.sbr
+.\Debug\cmd.sbr
+.\Debug\cmdAlias.sbr
+.\Debug\cmdApi.sbr
+.\Debug\cmdFlag.sbr
+.\Debug\cmdHist.sbr
+.\Debug\cmdUtils.sbr
+.\Debug\io.sbr
+.\Debug\ioRead.sbr
+.\Debug\ioReadBaf.sbr
+.\Debug\ioReadBench.sbr
+.\Debug\ioReadBlif.sbr
+.\Debug\ioReadEdif.sbr
+.\Debug\ioReadEqn.sbr
+.\Debug\ioReadPla.sbr
+.\Debug\ioReadVerilog.sbr
+.\Debug\ioUtil.sbr
+.\Debug\ioWriteBaf.sbr
+.\Debug\ioWriteBench.sbr
+.\Debug\ioWriteBlif.sbr
+.\Debug\ioWriteCnf.sbr
+.\Debug\ioWriteDot.sbr
+.\Debug\ioWriteEqn.sbr
+.\Debug\ioWriteGml.sbr
+.\Debug\ioWriteList.sbr
+.\Debug\ioWritePla.sbr
+.\Debug\ioWriteVerilog.sbr
+.\Debug\libSupport.sbr
+.\Debug\main.sbr
+.\Debug\mainFrame.sbr
+.\Debug\mainInit.sbr
+.\Debug\mainUtils.sbr
+.\Debug\cuddAddAbs.sbr
+.\Debug\cuddAddApply.sbr
+.\Debug\cuddAddFind.sbr
+.\Debug\cuddAddInv.sbr
+.\Debug\cuddAddIte.sbr
+.\Debug\cuddAddNeg.sbr
+.\Debug\cuddAddWalsh.sbr
+.\Debug\cuddAndAbs.sbr
+.\Debug\cuddAnneal.sbr
+.\Debug\cuddApa.sbr
+.\Debug\cuddAPI.sbr
+.\Debug\cuddApprox.sbr
+.\Debug\cuddBddAbs.sbr
+.\Debug\cuddBddCorr.sbr
+.\Debug\cuddBddIte.sbr
+.\Debug\cuddBridge.sbr
+.\Debug\cuddCache.sbr
+.\Debug\cuddCheck.sbr
+.\Debug\cuddClip.sbr
+.\Debug\cuddCof.sbr
+.\Debug\cuddCompose.sbr
+.\Debug\cuddDecomp.sbr
+.\Debug\cuddEssent.sbr
+.\Debug\cuddExact.sbr
+.\Debug\cuddExport.sbr
+.\Debug\cuddGenCof.sbr
+.\Debug\cuddGenetic.sbr
+.\Debug\cuddGroup.sbr
+.\Debug\cuddHarwell.sbr
+.\Debug\cuddInit.sbr
+.\Debug\cuddInteract.sbr
+.\Debug\cuddLCache.sbr
+.\Debug\cuddLevelQ.sbr
+.\Debug\cuddLinear.sbr
+.\Debug\cuddLiteral.sbr
+.\Debug\cuddMatMult.sbr
+.\Debug\cuddPriority.sbr
+.\Debug\cuddRead.sbr
+.\Debug\cuddRef.sbr
+.\Debug\cuddReorder.sbr
+.\Debug\cuddSat.sbr
+.\Debug\cuddSign.sbr
+.\Debug\cuddSolve.sbr
+.\Debug\cuddSplit.sbr
+.\Debug\cuddSubsetHB.sbr
+.\Debug\cuddSubsetSP.sbr
+.\Debug\cuddSymmetry.sbr
+.\Debug\cuddTable.sbr
+.\Debug\cuddUtil.sbr
+.\Debug\cuddWindow.sbr
+.\Debug\cuddZddCount.sbr
+.\Debug\cuddZddFuncs.sbr
+.\Debug\cuddZddGroup.sbr
+.\Debug\cuddZddIsop.sbr
+.\Debug\cuddZddLin.sbr
+.\Debug\cuddZddMisc.sbr
+.\Debug\cuddZddPort.sbr
+.\Debug\cuddZddReord.sbr
+.\Debug\cuddZddSetop.sbr
+.\Debug\cuddZddSymm.sbr
+.\Debug\cuddZddUtil.sbr
+.\Debug\epd.sbr
+.\Debug\mtrBasic.sbr
+.\Debug\mtrGroup.sbr
+.\Debug\parseCore.sbr
+.\Debug\parseStack.sbr
+.\Debug\dsdApi.sbr
+.\Debug\dsdCheck.sbr
+.\Debug\dsdLocal.sbr
+.\Debug\dsdMan.sbr
+.\Debug\dsdProc.sbr
+.\Debug\dsdTree.sbr
+.\Debug\reoApi.sbr
+.\Debug\reoCore.sbr
+.\Debug\reoProfile.sbr
+.\Debug\reoSift.sbr
+.\Debug\reoSwap.sbr
+.\Debug\reoTest.sbr
+.\Debug\reoTransfer.sbr
+.\Debug\reoUnits.sbr
+.\Debug\added.sbr
+.\Debug\solver.sbr
+.\Debug\msatActivity.sbr
+.\Debug\msatClause.sbr
+.\Debug\msatClauseVec.sbr
+.\Debug\msatMem.sbr
+.\Debug\msatQueue.sbr
+.\Debug\msatRead.sbr
+.\Debug\msatSolverApi.sbr
+.\Debug\msatSolverCore.sbr
+.\Debug\msatSolverIo.sbr
+.\Debug\msatSolverSearch.sbr
+.\Debug\msatSort.sbr
+.\Debug\msatVec.sbr
+.\Debug\fraigApi.sbr
+.\Debug\fraigCanon.sbr
+.\Debug\fraigFanout.sbr
+.\Debug\fraigFeed.sbr
+.\Debug\fraigMan.sbr
+.\Debug\fraigMem.sbr
+.\Debug\fraigNode.sbr
+.\Debug\fraigPrime.sbr
+.\Debug\fraigSat.sbr
+.\Debug\fraigTable.sbr
+.\Debug\fraigUtil.sbr
+.\Debug\fraigVec.sbr
+.\Debug\csat_apis.sbr
+.\Debug\fxu.sbr
+.\Debug\fxuCreate.sbr
+.\Debug\fxuHeapD.sbr
+.\Debug\fxuHeapS.sbr
+.\Debug\fxuList.sbr
+.\Debug\fxuMatrix.sbr
+.\Debug\fxuPair.sbr
+.\Debug\fxuPrint.sbr
+.\Debug\fxuReduce.sbr
+.\Debug\fxuSelect.sbr
+.\Debug\fxuSingle.sbr
+.\Debug\fxuUpdate.sbr
+.\Debug\rwrDec.sbr
+.\Debug\rwrEva.sbr
+.\Debug\rwrExp.sbr
+.\Debug\rwrLib.sbr
+.\Debug\rwrMan.sbr
+.\Debug\rwrPrint.sbr
+.\Debug\rwrUtil.sbr
+.\Debug\cutApi.sbr
+.\Debug\cutCut.sbr
+.\Debug\cutMan.sbr
+.\Debug\cutMerge.sbr
+.\Debug\cutNode.sbr
+.\Debug\cutOracle.sbr
+.\Debug\cutSeq.sbr
+.\Debug\cutTruth.sbr
+.\Debug\decAbc.sbr
+.\Debug\decFactor.sbr
+.\Debug\decMan.sbr
+.\Debug\decPrint.sbr
+.\Debug\decUtil.sbr
+.\Debug\simMan.sbr
+.\Debug\simSat.sbr
+.\Debug\simSeq.sbr
+.\Debug\simSupp.sbr
+.\Debug\simSwitch.sbr
+.\Debug\simSym.sbr
+.\Debug\simSymSat.sbr
+.\Debug\simSymSim.sbr
+.\Debug\simSymStr.sbr
+.\Debug\simUtils.sbr
+.\Debug\xyzBuild.sbr
+.\Debug\xyzCore.sbr
+.\Debug\xyzMan.sbr
+.\Debug\xyzMinEsop.sbr
+.\Debug\xyzMinMan.sbr
+.\Debug\xyzMinSop.sbr
+.\Debug\xyzMinUtil.sbr
+.\Debug\xyzTest.sbr
+.\Debug\fpga.sbr
+.\Debug\fpgaCore.sbr
+.\Debug\fpgaCreate.sbr
+.\Debug\fpgaCut.sbr
+.\Debug\fpgaCutUtils.sbr
+.\Debug\fpgaFanout.sbr
+.\Debug\fpgaLib.sbr
+.\Debug\fpgaMatch.sbr
+.\Debug\fpgaSwitch.sbr
+.\Debug\fpgaTime.sbr
+.\Debug\fpgaTruth.sbr
+.\Debug\fpgaUtils.sbr
+.\Debug\fpgaVec.sbr
+.\Debug\mapper.sbr
+.\Debug\mapperCanon.sbr
+.\Debug\mapperCore.sbr
+.\Debug\mapperCreate.sbr
+.\Debug\mapperCut.sbr
+.\Debug\mapperCutUtils.sbr
+.\Debug\mapperFanout.sbr
+.\Debug\mapperLib.sbr
+.\Debug\mapperMatch.sbr
+.\Debug\mapperRefs.sbr
+.\Debug\mapperSuper.sbr
+.\Debug\mapperSwitch.sbr
+.\Debug\mapperTable.sbr
+.\Debug\mapperTime.sbr
+.\Debug\mapperTree.sbr
+.\Debug\mapperTruth.sbr
+.\Debug\mapperUtils.sbr
+.\Debug\mapperVec.sbr
+.\Debug\mio.sbr
+.\Debug\mioApi.sbr
+.\Debug\mioFunc.sbr
+.\Debug\mioRead.sbr
+.\Debug\mioUtils.sbr
+.\Debug\super.sbr
+.\Debug\superAnd.sbr
+.\Debug\superGate.sbr
+.\Debug\superWrite.sbr
+.\Debug\pgaCore.sbr
+.\Debug\pgaMan.sbr
+.\Debug\pgaMatch.sbr
+.\Debug\pgaUtil.sbr
+.\Debug\extraBddKmap.sbr
+.\Debug\extraBddMisc.sbr
+.\Debug\extraBddSymm.sbr
+.\Debug\extraUtilBitMatrix.sbr
+.\Debug\extraUtilCanon.sbr
+.\Debug\extraUtilFile.sbr
+.\Debug\extraUtilMemory.sbr
+.\Debug\extraUtilMisc.sbr
+.\Debug\extraUtilProgress.sbr
+.\Debug\extraUtilReader.sbr
+.\Debug\st.sbr
+.\Debug\stmm.sbr
+.\Debug\cpu_stats.sbr
+.\Debug\cpu_time.sbr
+.\Debug\datalimit.sbr
+.\Debug\getopt.sbr
+.\Debug\pathsearch.sbr
+.\Debug\safe_mem.sbr
+.\Debug\strsav.sbr
+.\Debug\texpand.sbr
+.\Debug\mvc.sbr
+.\Debug\mvcApi.sbr
+.\Debug\mvcCompare.sbr
+.\Debug\mvcContain.sbr
+.\Debug\mvcCover.sbr
+.\Debug\mvcCube.sbr
+.\Debug\mvcDivide.sbr
+.\Debug\mvcDivisor.sbr
+.\Debug\mvcList.sbr
+.\Debug\mvcLits.sbr
+.\Debug\mvcMan.sbr
+.\Debug\mvcOpAlg.sbr
+.\Debug\mvcOpBool.sbr
+.\Debug\mvcPrint.sbr
+.\Debug\mvcSort.sbr
+.\Debug\mvcUtils.sbr
+.\Debug\msatOrderJ.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP14FB.tmp"
+Creating browse info file...
+<h3>Output Window</h3>
 
 
 
diff --git a/abc.rc b/abc.rc
index 4b2e5599..8a334225 100644
--- a/abc.rc
+++ b/abc.rc
@@ -74,4 +74,5 @@ alias compress  "b; rw -l; rwz -l; b; rwz -l; b"
 alias compress2 "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b"
 alias choice    "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2   "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
+alias try       "st; fpga; miter; fraig -rp"
 
diff --git a/mcnc_temp.genlib_temp b/mcnc_temp.genlib_temp
new file mode 100644
index 00000000..19f7a338
--- /dev/null
+++ b/mcnc_temp.genlib_temp
@@ -0,0 +1,67 @@
+# The genlib library "mcnc_temp.genlib".
+GATE         inv1       1.00   O=!a;
+    PIN         a        INV      1    999   0.90   0.00   0.90   0.00
+GATE         inv2       2.00   O=!a;
+    PIN         a        INV      2    999   1.00   0.00   1.00   0.00
+GATE         inv3       3.00   O=!a;
+    PIN         a        INV      3    999   1.10   0.00   1.10   0.00
+GATE         inv4       4.00   O=!a;
+    PIN         a        INV      4    999   1.20   0.00   1.20   0.00
+GATE        nand2       2.00   O=!(a*b);
+    PIN         a        INV      1    999   1.00   0.00   1.00   0.00
+    PIN         b        INV      1    999   1.00   0.00   1.00   0.00
+GATE        nand3       3.00   O=!(a*b*c);
+    PIN         a        INV      1    999   1.10   0.00   1.10   0.00
+    PIN         b        INV      1    999   1.10   0.00   1.10   0.00
+    PIN         c        INV      1    999   1.10   0.00   1.10   0.00
+GATE        nand4       4.00   O=!(a*b*c*d);
+    PIN         a        INV      1    999   1.40   0.00   1.40   0.00
+    PIN         b        INV      1    999   1.40   0.00   1.40   0.00
+    PIN         c        INV      1    999   1.40   0.00   1.40   0.00
+    PIN         d        INV      1    999   1.40   0.00   1.40   0.00
+GATE         nor2       2.00   O=!(a+b);
+    PIN         a        INV      1    999   1.40   0.00   1.40   0.00
+    PIN         b        INV      1    999   1.40   0.00   1.40   0.00
+GATE         nor3       3.00   O=!(a+b+c);
+    PIN         a        INV      1    999   2.40   0.00   2.40   0.00
+    PIN         b        INV      1    999   2.40   0.00   2.40   0.00
+    PIN         c        INV      1    999   2.40   0.00   2.40   0.00
+GATE         nor4       4.00   O=!(a+b+c+d);
+    PIN         a        INV      1    999   3.80   0.00   3.80   0.00
+    PIN         b        INV      1    999   3.80   0.00   3.80   0.00
+    PIN         c        INV      1    999   3.80   0.00   3.80   0.00
+    PIN         d        INV      1    999   3.80   0.00   3.80   0.00
+GATE         xora       5.00   O=a*!b+!a*b;
+    PIN         a    UNKNOWN      2    999   1.90   0.00   1.90   0.00
+    PIN         b    UNKNOWN      2    999   1.90   0.00   1.90   0.00
+GATE         xorb       5.00   O=!(a*b+!a*!b);
+    PIN         a    UNKNOWN      2    999   1.90   0.00   1.90   0.00
+    PIN         b    UNKNOWN      2    999   1.90   0.00   1.90   0.00
+GATE        xnora       5.00   O=a*b+!a*!b;
+    PIN         a    UNKNOWN      2    999   2.10   0.00   2.10   0.00
+    PIN         b    UNKNOWN      2    999   2.10   0.00   2.10   0.00
+GATE        xnorb       5.00   O=!(!a*b+a*!b);
+    PIN         a    UNKNOWN      2    999   2.10   0.00   2.10   0.00
+    PIN         b    UNKNOWN      2    999   2.10   0.00   2.10   0.00
+GATE        aoi21       3.00   O=!(a*b+c);
+    PIN         a        INV      1    999   1.60   0.00   1.60   0.00
+    PIN         b        INV      1    999   1.60   0.00   1.60   0.00
+    PIN         c        INV      1    999   1.60   0.00   1.60   0.00
+GATE        aoi22       4.00   O=!(a*b+c*d);
+    PIN         a        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         b        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         c        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         d        INV      1    999   2.00   0.00   2.00   0.00
+GATE        oai21       3.00   O=!((a+b)*c);
+    PIN         a        INV      1    999   1.60   0.00   1.60   0.00
+    PIN         b        INV      1    999   1.60   0.00   1.60   0.00
+    PIN         c        INV      1    999   1.60   0.00   1.60   0.00
+GATE        oai22       4.00   O=!((a+b)*(c+d));
+    PIN         a        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         b        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         c        INV      1    999   2.00   0.00   2.00   0.00
+    PIN         d        INV      1    999   2.00   0.00   2.00   0.00
+GATE          buf       1.00   O=a;
+    PIN         a     NONINV      1    999   1.00   0.00   1.00   0.00
+GATE         zero       0.00   O=CONST0;
+GATE          one       0.00   O=CONST1;
diff --git a/mcnc_temp.super b/mcnc_temp.super
new file mode 100644
index 00000000..31735b8b
--- /dev/null
+++ b/mcnc_temp.super
@@ -0,0 +1,42 @@
+#
+# Supergate library derived for "mcnc_temp.genlib_temp" on Sun Dec 25 06:29:48 2005.
+#
+# Command line: "super  -i 5  -l 1  -d 10000000.00  -a 10000000.00  -t 100    mcnc_temp.genlib_temp".
+#
+# The number of inputs      =          5.
+# The number of levels      =          1.
+# The maximum delay         = 10000000.00.
+# The maximum area          = 10000000.00.
+# The maximum runtime (sec) =        100.
+#
+# The number of attempts    =        860.
+# The number of supergates  =         20.
+# The number of functions   =          0.
+# The total functions       = 4294967296 (2^32).
+#
+# Generation time (sec)     =       0.01.
+#
+mcnc_temp.genlib_temp
+5
+20
+25       
+* xorb 1 0
+* nor4 2 1 0 3
+* nor3 2 1 0
+* oai22 2 1 0 3
+* oai22 2 0 1 3
+* aoi21 1 0 2
+* aoi22 2 3 1 0
+* nor2 1 0
+* oai22 2 3 1 0
+* aoi21 2 0 1
+* aoi22 2 0 1 3
+* aoi21 2 1 0
+* aoi22 2 1 0 3
+* oai21 1 0 2
+* oai21 2 0 1
+* oai21 2 1 0
+* nand2 1 0
+* nand3 2 1 0
+* nand4 2 1 0 3
+* xnora 1 0
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 53ad88c2..167e7552 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), 
                             Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
+{
+    Abc_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Abc_AigMiter_rec( pMan, ppObjs,           nObjs/2 );
+    pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
+    return Abc_AigOr( pMan, pObj1, pObj2 );
+}
+ 
 /**Function*************************************************************
 
   Synopsis    [Implements the miter.]
@@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 ***********************************************************************/
 Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
 {
+    int i;
+    if ( vPairs->nSize == 0 )
+        return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) );
+    assert( vPairs->nSize % 2 == 0 );
+    // go through the cubes of the node's SOP
+    for ( i = 0; i < vPairs->nSize; i += 2 )
+        vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    vPairs->nSize = vPairs->nSize/2;
+    return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
+{
     Abc_Obj_t * pMiter, * pXor;
     int i;
     assert( vPairs->nSize % 2 == 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 71b76cf6..70cd2e6c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     } 
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
+        return 0;
+    }
+
+/*
     if ( !Abc_NtkIsLogic(pNtk) )
     {
         fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
@@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkUnmap(pNtk);
     if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkSopToBdd(pNtk);
-
-    RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
-    if ( RetValue == -1 )
-        printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
-    else if ( RetValue == 0 )
-        printf( "The miter is SATISFIABLE.\n" );
+*/
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
+        if ( RetValue == -1 )
+            printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+        else if ( RetValue == 0 )
+            printf( "The miter is SATISFIABLE.\n" );
+        else
+            printf( "The miter is UNSATISFIABLE.\n" );
+    }
     else
-        printf( "The miter is UNSATISFIABLE.\n" );
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
+        if ( RetValue == -1 )
+            printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+        else if ( RetValue == 0 )
+            printf( "The miter is SATISFIABLE.\n" );
+        else
+            printf( "The miter is UNSATISFIABLE.\n" );
+        Abc_NtkDelete( pTemp );
+    }
     return 0;
 
 usage:
     fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
-    fprintf( pErr, "\t         solves the miter\n" );
+    fprintf( pErr, "\t         solves the combinational miter\n" );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-//    Abc_NtkDeriveEsops( pNtk );
-//    Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
-    printf( "This command is currently not used.\n" );
+    Abc_NtkTestEsop( pNtk );
+//    Abc_NtkTestSop( pNtk );
+//    printf( "This command is currently not used.\n" );
 
 /*
     // run the command
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 4a65659c..8c8636c5 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -27,6 +27,10 @@
 static int  Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 static int  Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 
+static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
+
+static nMuxes;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -129,7 +133,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     Vec_Str_t * vCube;
     Vec_Int_t * vVars;
     char * pSop0, * pSop1;
-    int i;
+    int i, clk = clock();
 
     assert( Abc_NtkIsBddLogic(pNtk) );
 
@@ -159,6 +163,8 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     }
 //    Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
 
+    PRT( "Creating solver", clock() - clk );
+
     // delete
     Vec_StrFree( vCube );
     Vec_IntFree( vVars );
@@ -291,6 +297,495 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 }
 
 
+
+
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Attempts to solve the miter using an internal SAT solver.]
+
+  Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+{
+    solver * pSat;
+    lbool   status;
+    int RetValue, clk;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+
+    if ( Abc_NtkPoNum(pNtk) > 1 )
+        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
+
+    // load clauses into the solver
+    clk = clock();
+    pSat = Abc_NtkMiterSatCreate2( pNtk );
+    if ( pSat == NULL )
+        return 1;
+//    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+
+    // simplify the problem
+    clk = clock();
+    status = solver_simplify(pSat);
+//    printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+    if ( status == 0 )
+    {
+        solver_delete( pSat );
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return 1;
+    }
+
+    // solve the miter
+    clk = clock();
+    if ( fVerbose )
+        pSat->verbosity = 1;
+    status = solver_solve( pSat, NULL, NULL, nSeconds );
+    if ( status == l_Undef )
+    {
+//        printf( "The problem timed out.\n" );
+        RetValue = -1;
+    }
+    else if ( status == l_True )
+    {
+//        printf( "The problem is SATISFIABLE.\n" );
+        RetValue = 0;
+    }
+    else if ( status == l_False )
+    {
+//        printf( "The problem is UNSATISFIABLE.\n" );
+        RetValue = 1;
+    }
+    else
+        assert( 0 );
+    PRT( "SAT solver time", clock() - clk );
+
+    // if the problem is SAT, get the counterexample
+    if ( status == l_True )
+    {
+        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+        pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
+        Vec_IntFree( vCiIds );
+    }
+    // free the solver
+    solver_delete( pSat );
+    return RetValue;
+}
+
+
+
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+//    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
+{
+    int fComp1, Var, Var1, i;
+//printf( "Adding AND %d.  (%d)    %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses );
+
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+
+//    nVars = solver_nvars(pSat);
+    Var = (int)pNode->pCopy;
+//    Var = pNode->Id;
+
+//    assert( Var  < nVars ); 
+    for ( i = 0; i < vSuper->nSize; i++ )
+    {
+        // get the predecessor nodes
+        // get the complemented attributes of the nodes
+        fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
+        // determine the variable numbers
+        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+//        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
+
+        // check that the variables are in the SAT manager
+//        assert( Var1 < nVars );
+
+        // suppose the AND-gate is A * B = C
+        // add !A => !C   or   A + !C
+    //  fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
+        Vec_IntPush( vVars, toLitCond(Var,  1     ) );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
+    }
+
+    // add A & B => C   or   !A + !B + C
+//  fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
+    vVars->nSize = 0;
+    for ( i = 0; i < vSuper->nSize; i++ )
+    {
+        // get the predecessor nodes
+        // get the complemented attributes of the nodes
+        fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
+        // determine the variable numbers
+        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+//        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
+        // add this variable to the array
+        Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
+    }
+    Vec_IntPush( vVars, toLitCond(Var, 0) );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars )
+{
+    int VarF, VarI, VarT, VarE, fCompT, fCompE;
+//printf( "Adding mux %d.         %d\n", pNode->Id, (int)pSat->solver_stats.clauses );
+
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_NodeIsMuxType( pNode ) );
+    // get the variable numbers
+    VarF = (int)pNode->pCopy;
+    VarI = (int)pNodeC->pCopy;
+    VarT = (int)Abc_ObjRegular(pNodeT)->pCopy;
+    VarE = (int)Abc_ObjRegular(pNodeE)->pCopy;
+//    VarF = (int)pNode->Id;
+//    VarI = (int)pNodeC->Id;
+//    VarT = (int)Abc_ObjRegular(pNodeT)->Id;
+//    VarE = (int)Abc_ObjRegular(pNodeE)->Id;
+
+    // get the complementation flags
+    fCompT = Abc_ObjIsComplement(pNodeT);
+    fCompE = Abc_ObjIsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+    // create four clauses
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarI,  1) );
+    Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
+    Vec_IntPush( vVars, toLitCond(VarF,  0) );
+    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        return 0;
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarI,  1) );
+    Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
+    Vec_IntPush( vVars, toLitCond(VarF,  1) );
+    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        return 0;
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarI,  0) );
+    Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
+    Vec_IntPush( vVars, toLitCond(VarF,  0) );
+    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        return 0;
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarI,  0) );
+    Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
+    Vec_IntPush( vVars, toLitCond(VarF,  1) );
+    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        return 0;
+
+    if ( VarT == VarE )
+    {
+        assert( fCompT == !fCompE );
+        return 1;
+    }
+
+    // two additional clauses
+    // t' & e' -> f'       t  + e   + f'
+    // t  & e  -> f        t' + e'  + f 
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarT,  0^fCompT) );
+    Vec_IntPush( vVars, toLitCond(VarE,  0^fCompE) );
+    Vec_IntPush( vVars, toLitCond(VarF,  1) );
+    if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+        return 0;
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLitCond(VarT,  1^fCompT) );
+    Vec_IntPush( vVars, toLitCond(VarE,  1^fCompE) );
+    Vec_IntPush( vVars, toLitCond(VarF,  0) );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
+{
+    int RetValue1, RetValue2, i;
+    // check if the node is visited
+    if ( Abc_ObjRegular(pNode)->fMarkB )
+    {
+        // check if the node occurs in the same polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == pNode )
+                return 1;
+        // check if the node is present in the opposite polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == Abc_ObjNot(pNode) )
+                return -1;
+        assert( 0 );
+        return 0;
+    }
+    // if the new node is complemented or a PI, another gate begins
+    if ( !fFirst )
+    if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) )
+    {
+        Vec_PtrPush( vSuper, pNode );
+        Abc_ObjRegular(pNode)->fMarkB = 1;
+        return 0;
+    }
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    // go through the branches
+    RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux );
+    RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(pNode), vSuper, 0, fStopAtMux );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
+{
+    int RetValue, i;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // collect the nodes in the implication supergate
+    Vec_PtrClear( vNodes );
+    RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
+    assert( vNodes->nSize > 1 );
+    // unmark the visited nodes
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
+    // if we found the node and its complement in the same implication supergate, 
+    // return empty set of nodes (meaning that we should use constant-0 node)
+    if ( RetValue == -1 )
+        vNodes->nSize = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
+    Vec_Ptr_t * vNodes, * vSuper;
+    Vec_Int_t * vVars;
+    int i, k, fUseMuxes = 1;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // start the data structures
+    vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
+    vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
+    vVars  = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
+
+    // add the clause for the constant node
+    pNode = Abc_NtkConst1(pNtk);
+    pNode->fMarkA = 1;
+    pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
+    Vec_PtrPush( vNodes, pNode );
+    Abc_NtkClauseTriv( pSat, pNode, vVars );
+
+    // collect the nodes that need clauses and top-level assignments
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        // get the fanin
+        pFanin = Abc_ObjFanin0(pNode);
+        // create the node's variable
+        if ( pFanin->fMarkA == 0 )
+        {
+            pFanin->fMarkA = 1;
+            pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+            Vec_PtrPush( vNodes, pFanin );
+        }
+        // add the trivial clause
+        if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
+            return 0;
+    }
+
+    // add the clauses
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        assert( !Abc_ObjIsComplement(pNode) );
+        if ( !Abc_NodeIsAigAnd(pNode) )
+            continue;
+//printf( "%d ", pNode->Id );
+
+        // add the clauses
+        if ( fUseMuxes && Abc_NodeIsMuxType(pNode) )
+        {
+            nMuxes++;
+
+            pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
+            Vec_PtrClear( vSuper );
+            Vec_PtrPush( vSuper, pNodeC );
+            Vec_PtrPush( vSuper, pNodeT );
+            Vec_PtrPush( vSuper, pNodeE );
+            // add the fanin nodes to explore
+            Vec_PtrForEachEntry( vSuper, pFanin, k )
+            {
+                pFanin = Abc_ObjRegular(pFanin);
+                if ( pFanin->fMarkA == 0 )
+                {
+                    pFanin->fMarkA = 1;
+                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+                    Vec_PtrPush( vNodes, pFanin );
+                }
+            }
+            // add the clauses
+            if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
+                return 0;
+        }
+        else
+        {
+            // get the supergate
+            Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper );
+            // add the fanin nodes to explore
+            Vec_PtrForEachEntry( vSuper, pFanin, k )
+            {
+                pFanin = Abc_ObjRegular(pFanin);
+                if ( pFanin->fMarkA == 0 )
+                {
+                    pFanin->fMarkA = 1;
+                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+                    Vec_PtrPush( vNodes, pFanin );
+                }
+            }
+            // add the clauses
+            if ( vSuper->nSize == 0 )
+            {
+                if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
+                    return 0;
+            }
+            else
+            {
+                if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
+                    return 0;
+            }
+        }
+    }
+
+    // delete
+    Vec_IntFree( vVars );
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vSuper );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
+{
+    solver * pSat;
+    Abc_Obj_t * pNode;
+    int RetValue, i, clk = clock();
+
+    nMuxes = 0;
+
+    pSat = solver_new();
+    RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        pNode->fMarkA = 0;
+    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+    if ( RetValue == 0 )
+    {
+        solver_delete(pSat);
+        return NULL;
+    }
+    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+    PRT( "Creating solver", clock() - clk );
+    return pSat;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 070c871d..b30a6452 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
+    Params.fFuncRed = 0;
+    Params.nPatsRand = 0;
+    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
@@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
+    Params.fFuncRed = 0;
+    Params.nPatsRand = 0;
+    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
index f18686ff..ea488068 100644
--- a/src/opt/xyz/xyz.h
+++ b/src/opt/xyz/xyz.h
@@ -46,6 +46,8 @@ struct Xyz_Man_t_
     Vec_Ptr_t *       vObjStrs;     // object structures
     void *            pMemory;      // memory for the internal data strctures
     Min_Man_t *       pManMin;      // the cub manager
+    int               fUseEsop;     // enables ESOPs
+    int               fUseSop;      // enables SOPs
     // arrays to map local variables
     Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
     Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
index a48f749e..e5089788 100644
--- a/src/opt/xyz/xyzCore.c
+++ b/src/opt/xyz/xyzCore.c
@@ -27,13 +27,19 @@
 static void        Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
 static int         Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
 static void        Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
-
+/*
 static int         Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
 static int         Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
 static int         Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
 static int         Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+*/
+
+static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj );
+static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -59,6 +65,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
 
     // create the manager
     p = Xyz_ManAlloc( pNtk, nFaninMax );
+    p->fUseEsop = fUseEsop;
+    p->fUseSop  = 1;//fUseSop;
     pNtk->pManCut = p;
 
     // perform mapping
@@ -69,6 +77,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
         pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
     else
         pNtkNew = Abc_NtkXyzDerive( p, pNtk );
+//    pNtkNew = NULL;
+
 
     Xyz_ManFree( p );
     pNtk->pManCut = NULL;
@@ -164,7 +174,10 @@ int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
         } 
 
         // traverse the cone starting from this node
-        Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+        if ( Abc_ObjGetSupp(pObj) == NULL )
+            Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+
+        // count the number of solved cones
         if ( Abc_ObjGetSupp(pObj) == NULL )
             fStop = 0;
         else
@@ -225,7 +238,7 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
 {
     Abc_Obj_t * pObj0, * pObj1;
     // return if the support is already computed
-    if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) )
+    if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
         return;
     // mark as visited
     pObj->fMarkB = 1;
@@ -236,9 +249,9 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
     Abc_NtkXyzCovers_rec( p, pObj0, vBoundary );
     Abc_NtkXyzCovers_rec( p, pObj1, vBoundary );
     // skip the node that spaced out
-    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||     // fanin is not ready
-         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||     // fanin is not ready
-         !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) )  // node's support or covers cannot be computed
+    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||  // fanin is not ready
+         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||  // fanin is not ready
+         !Abc_NodeXyzPropagate( p, pObj ) )           // node's support or covers cannot be computed
     {
         // save the nodes of the future boundary
         if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
@@ -331,6 +344,321 @@ Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * v
 
 /**Function*************************************************************
 
+  Synopsis    [Propagates all types of covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj )
+{
+    Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
+    Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
+    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
+    Abc_Obj_t * pObj0, * pObj1;
+    int fCompl0, fCompl1;
+
+    pObj0 = Abc_ObjFanin0( pObj );
+    pObj1 = Abc_ObjFanin1( pObj );
+
+    if ( pObj0->fMarkA )  Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
+    if ( pObj1->fMarkA )  Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
+
+    // get the resulting support
+    vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
+    vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
+    vSupp  = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
+
+    // quit if support if too large
+    if ( vSupp->nSize > p->nFaninMax )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // get the complemented attributes
+    fCompl0 = Abc_ObjFaninC0( pObj );
+    fCompl1 = Abc_ObjFaninC1( pObj );
+
+    // propagate ESOP
+    if ( p->fUseEsop )
+    {
+        // get the covers
+        pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
+        pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
+        if ( pCov0 && pCov1 )
+        {
+            // complement the first if needed
+            if ( !fCompl0 )
+                pCover0 = pCov0;
+            else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+                pCover0 = pCov0->pNext;
+            else
+                pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
+
+            // complement the second if needed
+            if ( !fCompl1 )
+                pCover1 = pCov1;
+            else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+                pCover1 = pCov1->pNext;
+            else
+                pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
+
+            // derive the new cover
+            pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize );
+        }
+    }
+    // propagate SOPs
+    if ( p->fUseSop )
+    {
+        // get the covers for the direct polarity
+        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
+        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
+        // derive the new cover
+        if ( pCover0 && pCover1 )
+            pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize );
+
+        // get the covers for the inverse polarity
+        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
+        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
+        // derive the new cover
+        if ( pCover0 && pCover1 )
+            pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize );
+    }
+
+    // if none of the covers can be computed quit
+    if ( !pCoverX && !pCoverP && !pCoverN )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // set the covers
+    assert( Abc_ObjGetSupp(pObj) == NULL );
+    Abc_ObjSetSupp( pObj, vSupp );
+    Abc_ObjSetCover( pObj, pCoverP, 0 );
+    Abc_ObjSetCover( pObj, pCoverN, 1 );
+    Abc_ObjSetCover2( pObj, pCoverX );
+//printf( "%3d : %4d  %4d  %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );
+
+    // count statistics
+    p->nSupps++;
+    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    Min_Cube_t * pCover;
+    int i, Val0, Val1;
+    assert( pCover0 && pCover1 );
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        // go through the support variables of the cubes
+        for ( i = 0; i < p->vPairs0->nSize; i++ )
+        {
+            Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
+            Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
+            if ( (Val0 & Val1) == 0 )
+                break;
+        }
+        // check disjointness
+        if ( i < p->vPairs0->nSize )
+            continue;
+
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+//Min_CoverWriteFile( pCover, "large", 1 );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+
+        // create the product cube
+        pCube = Min_CubeAlloc( p->pManMin );
+
+        // add the literals
+        pCube->nLits = 0;
+        for ( i = 0; i < nSupp; i++ )
+        {
+            if ( p->vComTo0->pArray[i] == -1 )
+                Val0 = 3;
+            else
+                Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+
+            if ( p->vComTo1->pArray[i] == -1 )
+                Val1 = 3;
+            else
+                Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+
+            if ( (Val0 & Val1) == 3 )
+                continue;
+
+            Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
+            pCube->nLits++;
+        }
+        // add the cube to storage
+        if ( fEsop ) 
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+
+    // minimize the cover
+    if ( fEsop ) 
+        Min_EsopMinimize( p->pManMin );
+    else
+        Min_SopMinimize( p->pManMin );
+    pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+    // quit if the cover is too large
+    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+    {
+/*        
+Min_CoverWriteFile( pCover, "large", 1 );
+        Min_CoverExpand( p->pManMin, pCover );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        Min_EsopMinimize( p->pManMin );
+        pCover = Min_CoverCollect( p->pManMin, nSupp );
+*/
+        Min_CoverRecycle( p->pManMin, pCover );
+        return NULL;
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    Min_Cube_t * pCover;
+    int i, Val0, Val1;
+    assert( pCover0 && pCover1 );
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    Min_CoverForEachCube( pCover0, pCube0 )
+    {
+        // create the cube
+        pCube = Min_CubeAlloc( p->pManMin );
+        pCube->nLits = 0;
+        for ( i = 0; i < p->vComTo0->nSize; i++ )
+        {
+            if ( p->vComTo0->pArray[i] == -1 )
+                continue;
+            Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+            if ( Val0 == 3 )
+                continue;
+            Min_CubeXorVar( pCube, i, Val0 ^ 3 );
+            pCube->nLits++;
+        }
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+        // add the cube to storage
+        if ( fEsop )
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        // create the cube
+        pCube = Min_CubeAlloc( p->pManMin );
+        pCube->nLits = 0;
+        for ( i = 0; i < p->vComTo1->nSize; i++ )
+        {
+            if ( p->vComTo1->pArray[i] == -1 )
+                continue;
+            Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+            if ( Val1 == 3 )
+                continue;
+            Min_CubeXorVar( pCube, i, Val1 ^ 3 );
+            pCube->nLits++;
+        }
+        if ( p->pManMin->nCubes > p->nCubesMax )
+        {
+            pCover = Min_CoverCollect( p->pManMin, nSupp );
+            Min_CoverRecycle( p->pManMin, pCover );
+            return NULL;
+        }
+        // add the cube to storage
+        if ( fEsop )
+            Min_EsopAddCube( p->pManMin, pCube );
+        else
+            Min_SopAddCube( p->pManMin, pCube );
+    }
+
+    // minimize the cover
+    if ( fEsop ) 
+        Min_EsopMinimize( p->pManMin );
+    else
+        Min_SopMinimize( p->pManMin );
+    pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+    // quit if the cover is too large
+    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+    {
+        Min_CoverRecycle( p->pManMin, pCover );
+        return NULL;
+    }
+    return pCover;
+}
+
+
+
+
+
+
+
+#if 0
+
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -581,7 +909,7 @@ int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pC
             pCube->nLits++;
         }
         // add the cube to storage
-        while ( Min_EsopAddCube( p->pManMin, pCube ) );
+        Min_EsopAddCube( p->pManMin, pCube );
     }
     return 1;
 }
@@ -642,7 +970,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
             if ( p->pManMin->nCubes >= p->nCubesMax )
                 return 0;
             // add the cube to storage
-            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+            Min_EsopAddCube( p->pManMin, pCube );
         }
     }
     if ( pCover1 )
@@ -665,7 +993,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
             if ( p->pManMin->nCubes >= p->nCubesMax )
                 return 0;
             // add the cube to storage
-            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+            Min_EsopAddCube( p->pManMin, pCube );
         }
     }
     return 1;
@@ -688,7 +1016,7 @@ int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCove
 }
 
 
-
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
index 22950bfd..656612aa 100644
--- a/src/opt/xyz/xyzInt.h
+++ b/src/opt/xyz/xyzInt.h
@@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa
 
 /*=== xyzMinEsop.c ==========================================================*/
 extern void         Min_EsopMinimize( Min_Man_t * p );
-extern int          Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void         Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
 /*=== xyzMinSop.c ==========================================================*/
 extern void         Min_SopMinimize( Min_Man_t * p );
-extern int          Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void         Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
 /*=== xyzMinMan.c ==========================================================*/
 extern Min_Man_t *  Min_ManAlloc( int nVars );
 extern void         Min_ManClean( Min_Man_t * p, int nSupp );
@@ -92,8 +92,10 @@ extern void         Min_ManFree( Min_Man_t * p );
 /*=== xyzMinUtil.c ==========================================================*/
 extern void         Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
 extern void         Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
+extern void         Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
 extern void         Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
 extern void         Min_CoverCheck( Min_Man_t * p );
+extern int          Min_CubeCheck( Min_Cube_t * pCube );
 extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
 extern void         Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
 extern int          Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
@@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
     Min_Cube_t * pCube;
     pCube = Min_CubeAlloc( p );
     memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+    pCube->nLits = pCopy->nLits;
     return pCube;
 }
 
@@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms the cube into the result of distance-1 merging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
+{
+    int w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+        pCube->uData[w] |= pDist->uData[w];
+}
+
 
 
 /**Function*************************************************************
@@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
 
 /**Function*************************************************************
 
-  Synopsis    [Check if the cube is equal or dist1 or contained.]
+  Synopsis    [Returns 1 if the given cube is contained in one of the cubes of the cover.]
 
   Description []
                
@@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
+static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    Min_Cube_t * pCube;
+    Min_Cube_t * pThis;
     int i;
-    // check identity
-    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
-        if ( Min_CubesAreEqual( pCube, pNew ) )
+/*
+    // this cube cannot be equal to any cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeWrite( stdout, pCube );
+            assert( 0 );
+        }
+    }
+*/
+    // try to find a containing cube
+    for ( i = 0; i <= (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        // skip the bubble
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
             return 1;
-    // check containment
-    for ( i = 0; i < (int)pNew->nLits; i++ )
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-            if ( Min_CubeIsContained( pCube, pNew ) )
-                return 1;
+    }
     return 0;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Check if the cube is equal or dist1 or contained.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
-{
-    Min_Cube_t * pCube;
-    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
-        if ( Min_CubesDistOne( pCube, pNew, NULL ) )
-            return pCube;
-    return NULL;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
index 114e28a6..839e2410 100644
--- a/src/opt/xyz/xyzMinEsop.c
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p )
 
   Synopsis    [Performs one round of rewriting using distance 2 cubes.]
 
-  Description []
+  Description [The weakness of this procedure is that it tries each cube
+  with only one distance-2 cube. If this pair does not lead to improvement
+  the cube is inserted into the cover anyhow, and we try another pair.
+  A possible improvement would be to try this cube with all distance-2
+  cubes, until an improvement is found, or until all such cubes are tried.]
                
   SideEffects []
 
@@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p )
 
         // add the cubes
         nCubesOld = p->nCubes;
-        while ( Min_EsopAddCube( p, pCube ) );
-        while ( Min_EsopAddCube( p, pThis ) );
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
         // check if the cubes were absorbed
         if ( p->nCubes < nCubesOld + 2 )
             continue;
@@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p )
         pThis->nLits += (v11 != 3);
 
         // add them anyhow
-        while ( Min_EsopAddCube( p, pCube ) );
-        while ( Min_EsopAddCube( p, pThis ) );
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
     }
 //    printf( "Pairs = %d  ", nPairs );
 }
@@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p )
 
   Synopsis    [Adds the cube to storage.]
 
-  Description [If the distance one cube is found, returns the transformed
-  cube. If there is no distance one, adds the given cube to storage.
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.
   Do not forget to clean the storage!]
                
   SideEffects []
@@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
 {
     Min_Cube_t * pThis, ** ppPrev;
     // try to find the identical cube
@@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_EsopAddCubeInt( p, pCube ) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
index 423564c1..20314698 100644
--- a/src/opt/xyz/xyzMinMan.c
+++ b/src/opt/xyz/xyzMinMan.c
@@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars )
     pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );   
     pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
     pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    Min_ManClean( pMan, nVars );
     return pMan;
 }
 
diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
index 1c5951fe..a5d57c66 100644
--- a/src/opt/xyz/xyzMinSop.c
+++ b/src/opt/xyz/xyzMinSop.c
@@ -52,10 +52,11 @@ void Min_SopMinimize( Min_Man_t * p )
         nCubesOld = p->nCubes;
         Min_SopRewrite( p );
         nIter++;
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
     }
     while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+//    printf( "\n" );
 
-//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
 }
 
 /**Function*************************************************************
@@ -74,8 +75,17 @@ void Min_SopRewrite( Min_Man_t * p )
     Min_Cube_t * pCube, ** ppPrev;
     Min_Cube_t * pThis, ** ppPrevT;
     Min_Cube_t * pTemp;
-    int v00, v01, v10, v11, Var0, Var1, Index;
+    int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
     int nPairs = 0;
+/*    
+    {
+        Min_Cube_t * pCover;
+        pCover = Min_CoverCollect( p, p->nVars );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCover );
+        Min_CoverExpand( p, pCover );
+    }
+*/
 
     // insert the bubble before the first cube
     p->pBubble->pNext = p->ppStore[0];
@@ -127,7 +137,11 @@ void Min_SopRewrite( Min_Man_t * p )
             continue;
         }
         nPairs++;
-
+/*
+printf( "\n" );
+Min_CubeWrite( stdout, pCube );
+Min_CubeWrite( stdout, pThis );
+*/
         // remove the cubes, insert the bubble instead of pCube
         *ppPrevT = pThis->pNext;
         *ppPrev = p->pBubble;
@@ -135,6 +149,8 @@ void Min_SopRewrite( Min_Man_t * p )
         p->pBubble->nLits = pCube->nLits;
         p->nCubes -= 2;
 
+        assert( pCube != p->pBubble && pThis != p->pBubble );
+
 
         // save the dist2 parameters
         v00 = Min_CubeGetVar( pCube, Var0 );
@@ -145,22 +161,83 @@ void Min_SopRewrite( Min_Man_t * p )
         assert( v00 != 3   || v01 != 3 );
         assert( v10 != 3   || v11 != 3 );
 
-        // skip the case when rewriting is impossible
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // consider the case when both cubes have non-empty literals
         if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+        {
+            assert( v00 == (v10 ^ 3) );
+            assert( v01 == (v11 ^ 3) );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, 3 );
+            Min_CubeXorVar( pCube, Var1, 3 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+            // check if this cube is contained
+            fCont1 = Min_CoverContainsCube( p, pCube );
+            // undo the change
+            Min_CubeXorVar( pCube, Var1, 3 );
+
+            // check if the cubes can be overwritten
+            if ( fCont0 && fCont1 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits -= 2;
+                Min_SopAddCube( p, pCube );
+            }
+            else if ( fCont0 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else if ( fCont1 )
+            {
+                // expand both cubes and add them
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+                Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
+                pThis->nLits--;
+                Min_SopAddCube( p, pThis );
+            }
+            else
+            {
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
+            // otherwise, no change is possible
             continue;
+        }
 
         // if one of them does not have DC lit, move it
         if ( v00 != 3 && v01 != 3 )
         {
+            assert( v10 == 3 || v11 == 3 );
             pTemp = pCube; pCube = pThis; pThis = pTemp;
             Index = v00; v00 = v10; v10 = Index;
             Index = v01; v01 = v11; v11 = Index;
         }
 
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
         // make sure the first cube has first var DC
         if ( v00 != 3 )
         {
@@ -174,13 +251,93 @@ void Min_SopRewrite( Min_Man_t * p )
         if ( v00 == 3 && v11 == 3 )
         {
             assert( v01 != 3 && v10 != 3 );
-            // try two reduced cubes
-
+            // try the remaining minterm
+            // create the temporary cube equal to the first corner
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits++;
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pCube );
+            // undo the cube transformations
+            Min_CubeXorVar( pCube, Var0, v10 );
+            Min_CubeXorVar( pCube, Var1, 3   );
+            pCube->nLits--;
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try two reduced cubes
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // remember the cubes
+                nCubesOld = p->nCubes;
+                Min_SopAddCube( p, pCube );
+                // check if the cube is absorbed
+                if ( p->nCubes < nCubesOld + 1 )
+                { // absorbed - add the second cube
+                    Min_SopAddCube( p, pThis );
+                }
+                else
+                { // remove this cube, and try another one
+                    assert( pCube == p->ppStore[pCube->nLits] );
+                    p->ppStore[pCube->nLits] = pCube->pNext;
+                    p->nCubes--;
+
+                    // return the cube to the previous state
+                    Min_CubeXorVar( pCube, Var0, v10 );
+                    pCube->nLits--;
+
+                    // generate another reduced cube
+                    Min_CubeXorVar( pThis, Var1, v01 );
+                    pThis->nLits++;
+
+                    // add both cubes
+                    Min_SopAddCube( p, pCube );
+                    Min_SopAddCube( p, pThis );
+                }
+            }
         }
         else // the first cube has DC lit
         {
             assert( v01 != 3 && v10 != 3 && v11 != 3 );
-            // try reduced and expanded cube
+            // try the remaining minterm
+            // create the temporary cube equal to the minterm
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check if this cube is contained
+            fCont0 = Min_CoverContainsCube( p, pThis );
+            // undo the cube transformations
+            Min_CubeXorVar( pThis, Var0, 3 );
+            // check the case when both are covered
+            if ( fCont0 )
+            {
+                // one of the cubes can be recycled, the other expanded and added
+                Min_CubeRecycle( p, pThis );
+                // remove the literals
+                Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+                pCube->nLits--;
+                Min_SopAddCube( p, pCube );
+            }
+            else
+            {
+                // try reshaping the cubes
+                // reduce the first cube
+                Min_CubeXorVar( pCube, Var0, v10 );
+                pCube->nLits++;
+                // expand the second cube
+                Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+                pThis->nLits--;
+                // add both cubes
+                Min_SopAddCube( p, pCube );
+                Min_SopAddCube( p, pThis );
+            }
         }
     }
 //    printf( "Pairs = %d  ", nPairs );
@@ -188,26 +345,80 @@ void Min_SopRewrite( Min_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds cube to the SOP cover stored in the manager.]
 
-  Description []
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    return 1;
-}
-
+    Min_Cube_t * pThis, * pThis2, ** ppPrev;
+    int i;
+    // try to find the identical cube
+    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find a containing cube
+    for ( i = 0; i < (int)pCube->nLits; i++ )
+    Min_CoverForEachCube( p->ppStore[i], pThis )
+    {
+        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+        {
+            Min_CubeRecycle( p, pCube );
+            return 0;
+        }
+    }
+    // try to find distance one in the same bin
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, NULL ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransformOr( pCube, pThis );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
 
+    // clean the other cubes using this one
+    for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
+    {
+        ppPrev = &p->ppStore[i];
+        Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
+        {
+            if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
+            {
+                *ppPrev = pThis->pNext;
+                Min_CubeRecycle( p, pThis );
+                p->nCubes--;
+            }
+            else
+                ppPrev = &pThis->pNext;
+        }
+    }
 
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds the cube to storage.]
 
   Description []
                
@@ -216,27 +427,18 @@ int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
   SeeAlso     []
 
 ***********************************************************************/
-void Min_SopDist1Merge( Min_Man_t * p )
+void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
 {
-    Min_Cube_t * pCube, * pCube2, * pCubeNew;
-    int i;
-    for ( i = p->nVars; i >= 0; i-- )
-    {
-        Min_CoverForEachCube( p->ppStore[i], pCube )
-        Min_CoverForEachCube( pCube->pNext, pCube2 )
-        {
-            assert( pCube->nLits == pCube2->nLits );
-            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
-                continue;
-            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
-            assert( pCubeNew->nLits == pCube->nLits - 1 );
-            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
-            p->ppStore[pCubeNew->nLits] = pCubeNew;
-            p->nCubes++;
-        }
-    }
+    assert( Min_CubeCheck( pCube ) );
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_SopAddCubeInt( p, pCube ) );
 }
 
+
+
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -286,6 +488,38 @@ void Min_SopContain( Min_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, * pCubeNew;
+    int i;
+    for ( i = p->nVars; i >= 0; i-- )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCube( pCube->pNext, pCube2 )
+        {
+            assert( pCube->nLits == pCube2->nLits );
+            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+                continue;
+            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+            assert( pCubeNew->nLits == pCube->nLits - 1 );
+            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+            p->ppStore[pCubeNew->nLits] = pCubeNew;
+            p->nCubes++;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
 {
      Vec_Int_t * vVars;
@@ -334,6 +568,46 @@ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
      return Min_CoverCollect( p, p->nVars );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pThis;
+    int i;
+
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, 2*0+1 );
+    Min_CubeXorBit( pCube, 2*1+1 );
+    Min_CubeXorBit( pCube, 2*2+0 );
+    Min_CubeXorBit( pCube, 2*3+0 );
+    Min_CubeXorBit( pCube, 2*4+0 );
+    Min_CubeXorBit( pCube, 2*5+1 );
+    Min_CubeXorBit( pCube, 2*6+1 );
+    pCube->nLits = 7;
+
+//    Min_CubeWrite( stdout, pCube );
+
+    // check that the cubes contain it
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pThis )
+            if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                return 1;
+            }
+    Min_CubeRecycle( p, pCube );
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
index 0aebb815..9ec5f83f 100644
--- a/src/opt/xyz/xyzMinUtil.c
+++ b/src/opt/xyz/xyzMinUtil.c
@@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
   SeeAlso     []
 
 ***********************************************************************/
+void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        {
+            printf( "%2d : ", i );
+            if ( pCube == p->pBubble )
+            {
+                printf( "Bubble\n" );
+                continue;
+            }
+            Min_CubeWrite( pFile, pCube );
+        }
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
 {
     char Buffer[1000];
     Min_Cube_t * pCube;
     FILE * pFile;
     int i;
-    sprintf( Buffer, "%s.esop", pName );
+    sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
     for ( i = strlen(Buffer) - 1; i >= 0; i-- )
         if ( Buffer[i] == '<' || Buffer[i] == '>' )
             Buffer[i] = '_';
@@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+  Synopsis    []
 
   Description []
                
@@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CubeCheck( Min_Cube_t * pCube )
+{
+    int i;
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeGetVar( pCube, i ) == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converts the cover from the sorted structure.]
 
   Description []
@@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
             assert( i == (int)pCube->nLits );
             *ppTail = pCube; 
             ppTail = &pCube->pNext;
+            assert( pCube->uData[0] ); // not a bubble
         }
     }
     *ppTail = NULL;
diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
index 6c0a63f3..38580790 100644
--- a/src/opt/xyz/xyzTest.c
+++ b/src/opt/xyz/xyzTest.c
@@ -39,11 +39,377 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
+Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
 {
-    return NULL;
+    Min_Cube_t * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
+{
+    Min_Cube_t * pCover;
+    Min_Cube_t * pThis, * pCube;
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // add the cubes to storage
+    Min_CoverForEachCube( pCover0, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_CoverForEachCube( pCover1, pThis )
+    {
+        pCube = Min_CubeDup( p, pThis );
+        Min_SopAddCube( p, pCube );
+    }
+    Min_SopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCov0[2], * pCov1[2];
+    Min_Cube_t * pCoverP, * pCoverN;
+    Abc_Obj_t * pObj;
+    int i, nCubes, fCompl0, fCompl1;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+    {
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+        pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
+    }
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // get the complements
+        fCompl0 = Abc_ObjFaninC0(pObj);
+        fCompl1 = Abc_ObjFaninC1(pObj);
+        // get the covers
+        pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
+        pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
+        pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
+        pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
+        // compute the covers
+        pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
+        pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
+        // set the covers
+        pObj->pCopy = (Abc_Obj_t *)pCoverP;
+        pObj->pNext = (Abc_Obj_t *)pCoverN;
+    }
+
+     nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
+
+/*
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverP );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverN );
+*/
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    Min_CoverExpand( p, pCoverP );
+//    Min_SopMinimize( p );
+//    pCoverP = Min_CoverCollect( p, p->nVars );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    nCubes = Min_CoverCountCubes(pCoverP);
+
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = pObj->pNext = NULL;
+
+//    Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverP );
+//    printf( "\n" );
+//    Min_CoverWrite( stdout, pCoverN );
+    return nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestSop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkCleanNext(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 )
+{
+    Min_Cube_t * pCover0, * pCover1, * pCover;
+    Min_Cube_t * pCube0, * pCube1, * pCube;
+
+    // complement the first if needed
+    if ( !fComp0 )
+        pCover0 = pCov0;
+    else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+        pCover0 = pCov0->pNext;
+    else
+        pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
+
+    // complement the second if needed
+    if ( !fComp1 )
+        pCover1 = pCov1;
+    else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+        pCover1 = pCov1->pNext;
+    else
+        pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
+
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return NULL;
+
+    // clean storage
+    Min_ManClean( p, p->nVars );
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+            continue;
+        pCube = Min_CubesProduct( p, pCube0, pCube1 );
+        // add the cube to storage
+        Min_EsopAddCube( p, pCube );
+    }
+ 
+    if ( p->nCubes > 10 )
+    {
+//        printf( "(%d,", p->nCubes );
+        Min_EsopMinimize( p );
+//        printf( "%d) ", p->nCubes );
+    }
+
+    pCover = Min_CoverCollect( p, p->nVars );
+    assert( p->nCubes == Min_CoverCountCubes(pCover) );
+
+//    if ( p->nCubes > 1000 )
+//        printf( "%d ", p->nCubes );
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // set elementary vars
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+
+    // get the cover for each node in the array
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pCover = Abc_NodeDeriveCover( p,  
+            (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,  
+            (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
+            Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        pObj->pCopy = (Abc_Obj_t *)pCover;
+        if ( p->nCubes > 3000 )
+            return -1;
+    }
+
+    // add complement if needed
+    if ( Abc_ObjFaninC0(pRoot) )
+    {
+        if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
+        {
+            pCube = pCover;
+            pCover = pCover->pNext;
+            Min_CubeRecycle( p, pCube );
+            p->nCubes--;
+        }
+        else
+        {
+            pCube = Min_CubeAlloc( p );
+            pCube->pNext = pCover;
+            p->nCubes++;
+        }
+    }
+/*
+    Min_CoverExpand( p, pCover );
+    Min_EsopMinimize( p );
+    pCover = Min_CoverCollect( p, p->nVars );
+*/
+    // clean the copy fields
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = NULL;
+
+//    Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
+//    Min_CoverWrite( stdout, pCover );
+    return p->nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTestEsop( Abc_Ntk_t * pNtk )
+{
+    Min_Man_t * p;
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nCubes;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    Abc_NtkCleanCopy(pNtk);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+        {
+            printf( "%-20s :  Trivial.\n", Abc_ObjName(pObj) );
+            continue;
+        }
+
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+        printf( "%20s :  Cone = %5d.  Supp = %5d.  ", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+//        if ( vSupp->nSize <= 128 )
+        {
+            p = Min_ManAlloc( vSupp->nSize );
+            nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
+            printf( "Cubes = %5d.  ", nCubes );
+            Min_ManFree( p );
+        }
+        printf( "\n" );
+
+
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index b82601c4..9618603c 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -52,8 +52,9 @@ static const lbool l_Undef   =  0;
 static const lbool l_True    =  1;
 static const lbool l_False   = -1;
 
-static inline lit neg   (lit l) { return l ^ 1; }
-static inline lit toLit (int v) { return v + v; }
+static inline lit neg       (lit l)        { return l ^ 1; }
+static inline lit toLit     (int v)        { return v + v; }
+static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
 
 //=================================================================================================
 // Public interface:
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 97da413d..fab01368 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
             return p1;
         return Fraig_Not(pMan->pConst1);
     }
-
+/*
     // check for less trivial cases
     if ( Fraig_IsComplement(p1) )
     {
@@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
             return Fraig_Not(pMan->pConst1);
         }
     }
-
+*/
     // perform level-one structural hashing
     if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
     {
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index bc60e4e9..13f6b50b 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
 // The best way seems to be fanins followed by fanouts. Slight changes to this order
 // leads to big degradation in quality.
 
+static int nMuxes;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
     }
     if ( p->fVerboseP ) 
     {
-        PRT( "Final miter proof time", clock() - clk );
+//        PRT( "Final miter proof time", clock() - clk );
     }
 }
 
@@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
     }
 */
 
+    nMuxes = 0;
+
 
     // get the logic cone
 clk = clock();
@@ -202,6 +206,9 @@ clk = clock();
 //    Fraig_PrepareCones( p, pOld, pNew );
 p->timeTrav += clock() - clk;
 
+//    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
+//    PRT( "Time", clock() - clk );
+
 if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
@@ -226,6 +233,8 @@ clk = clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
 
+Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
+
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += clock() - clk;
@@ -284,6 +293,7 @@ p->time3 += clock() - clk;
 clk = clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += clock() - clk;
+
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += clock() - clk;
@@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
     Fraig_PrepareCones_rec( pMan, pNew );
     Fraig_PrepareCones_rec( pMan, pOld );
 
+
 /*
     nVars = Msat_IntVecReadSize( pMan->vVarsInt );
     pVars = Msat_IntVecReadArray( pMan->vVarsInt );
@@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
                 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
                 Fraig_SupergateAddClausesMux( pMan, pNode );
 //                Fraig_DetectFanoutFreeConeMux( pMan, pNode );
+
+                nMuxes++;
             }
             else
             {
@@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
     // t  + e   + f'
     // t' + e'  + f 
 
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
     Msat_IntVecClear( p->vProj );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
@@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
     assert( RetValue );
+
 }
 
 
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 37e0bbeb..40028784 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -87,6 +87,7 @@ extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
 extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
 // access to the solver internal data
 extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
+extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
 extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
 extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
 extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index f944ed81..62b9ecad 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         // nSeenId - 1 stands for negative
         // nSeenId     stands for positive
         // Remove false literals
+
+        // there is a bug here!!!!
+        // when the same var in opposite polarities is given, it drops one polarity!!!
+
         for ( i = j = 0; i < nLits; i++ ) {
             // get the corresponding variable
             Var  = MSAT_LIT2VAR(pLits[i]);
@@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         {
             Msat_SolverVarBumpActivity( p, pLits[i] );
 //            Msat_SolverVarBumpActivity( p, pLits[i] );
+            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
         }
     }
 
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index ef2375a7..3dfe2109 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -151,6 +151,7 @@ struct Msat_Solver_t_
     int                 nSeenId;     // the id of current seeing
     Msat_IntVec_t *     vReason;     // the temporary array of literals
     Msat_IntVec_t *     vTemp;       // the temporary array of literals
+    int *               pFreq;       // the number of times each var participated in conflicts
 
     // the memory manager
     Msat_MmStep_t *     pMem;
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index dd3a5a43..4a721487 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
 
 ***********************************************************************/
 int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;     }
+int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;     }
 int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc;}
 int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
 int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;    }
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index ed228b33..5f13694b 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
     int64 nConflictsOld = p->Stats.nConflicts;
     int64 nDecisionsOld = p->Stats.nDecisions;
 
+    p->pFreq = ALLOC( int, p->nVarsAlloc );
+    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
+ 
     if ( vAssumps )
     {
         int * pAssumps, nAssumps, i;
@@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
     }
     Msat_SolverCancelUntil( p, 0 );
     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
+/*
+    PRT( "True solver runtime", clock() - timeStart );
+    // print the statistics
+    {
+        int i, Counter = 0;
+        for ( i = 0; i < p->nVars; i++ )
+            if ( p->pFreq[i] > 0 )
+            {
+                printf( "%d ", p->pFreq[i] );
+                Counter++;
+            }
+        if ( Counter )
+            printf( "\n" );
+        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
+        PRT( "Time", clock() - timeStart );
+    }
+*/
     return Status;
 }