25 files changed, 3481 insertions, 82 deletions

diff --git a/Makefile b/Makefile
index 93749444..99dadb06 100644
--- a/Makefile
+++ b/Makefile
@@ -19,6 +19,7 @@ MODULES := \
 	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/mfs \
 	src/opt/sim src/opt/ret src/opt/res src/opt/lpk src/opt/fret \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
+	src/sat/psat \
 	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
 	src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
diff --git a/abc.dsp b/abc.dsp
index cfd72ed8..a8f63e61 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -50,7 +50,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 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 /machine:I386
-# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe"
+# ADD LINK32 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 m114pr.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe" /libpath:"lib"
 
 !ELSEIF  "$(CFG)" == "abc - Win32 Debug"
 
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -75,7 +75,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 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 /debug /machine:I386 /pdbtype:sept
-# ADD LINK32 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 /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
+# ADD LINK32 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 m114pd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept /libpath:"lib"
 
 !ENDIF 
 
@@ -1245,6 +1245,22 @@ SOURCE=.\src\sat\proof\pr.c
 SOURCE=.\src\sat\proof\pr.h
 # End Source File
 # End Group
+# Begin Group "psat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\psat\m114p.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\psat\m114p_types.h
+# End Source File
+# End Group
+# Begin Group "nsat"
+
+# PROP Default_Filter ""
+# End Group
 # End Group
 # Begin Group "opt"
 
diff --git a/abclib.dsp b/abclib.dsp
new file mode 100644
index 00000000..df244f0f
--- /dev/null
+++ b/abclib.dsp
@@ -0,0 +1,2844 @@
+# Microsoft Developer Studio Project File - Name="abclib" - Package Owner=<4>
+# Microsoft Developer Studio Generated Build File, Format Version 6.00
+# ** DO NOT EDIT **
+
+# TARGTYPE "Win32 (x86) Static Library" 0x0104
+
+CFG=abclib - Win32 Debug
+!MESSAGE This is not a valid makefile. To build this project using NMAKE,
+!MESSAGE use the Export Makefile command and run
+!MESSAGE 
+!MESSAGE NMAKE /f "abclib.mak".
+!MESSAGE 
+!MESSAGE You can specify a configuration when running NMAKE
+!MESSAGE by defining the macro CFG on the command line. For example:
+!MESSAGE 
+!MESSAGE NMAKE /f "abclib.mak" CFG="abclib - Win32 Debug"
+!MESSAGE 
+!MESSAGE Possible choices for configuration are:
+!MESSAGE 
+!MESSAGE "abclib - Win32 Release" (based on "Win32 (x86) Static Library")
+!MESSAGE "abclib - Win32 Debug" (based on "Win32 (x86) Static Library")
+!MESSAGE 
+
+# Begin Project
+# PROP AllowPerConfigDependencies 0
+# PROP Scc_ProjName ""
+# PROP Scc_LocalPath ""
+CPP=cl.exe
+RSC=rc.exe
+
+!IF  "$(CFG)" == "abclib - Win32 Release"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 0
+# PROP BASE Output_Dir "abclib___Win32_Release"
+# PROP BASE Intermediate_Dir "abclib___Win32_Release"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 0
+# PROP Output_Dir "abclib\ReleaseLib"
+# PROP Intermediate_Dir "abclib\ReleaseLib"
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
+# ADD BASE RSC /l 0x409 /d "NDEBUG"
+# ADD RSC /l 0x409 /d "NDEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LIB32=link.exe -lib
+# ADD BASE LIB32 /nologo
+# ADD LIB32 /nologo /out:"abclib\abclib_release.lib"
+
+!ELSEIF  "$(CFG)" == "abclib - Win32 Debug"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 1
+# PROP BASE Output_Dir "abclib___Win32_Debug"
+# PROP BASE Intermediate_Dir "abclib___Win32_Debug"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 1
+# PROP Output_Dir "abclib\DebugLib"
+# PROP Intermediate_Dir "abclib\DebugLib"
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
+# ADD BASE RSC /l 0x409 /d "_DEBUG"
+# ADD RSC /l 0x409 /d "_DEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LIB32=link.exe -lib
+# ADD BASE LIB32 /nologo
+# ADD LIB32 /nologo /out:"abclib\abclib_debug.lib"
+
+!ENDIF 
+
+# Begin Target
+
+# Name "abclib - Win32 Release"
+# Name "abclib - Win32 Debug"
+# Begin Group "Source Files"
+
+# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
+# Begin Group "base"
+
+# PROP Default_Filter ""
+# Begin Group "abc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abc\abc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcBlifMv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFanio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcHie.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcLatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcMinBase.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNames.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNetlist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcShow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abc\abcUtil.c
+# End Source File
+# End Group
+# Begin Group "abci"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\abci\abc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcAttach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcAuto.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcBmc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCas.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcClpBdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcClpSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDar.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDebug.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDress.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcEspresso.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcExtract.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFpgaFast.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFraig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcFxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcGen.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcHaig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcIf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcIvy.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcLut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMeasure.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMini.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMiter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMulti.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcMv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcOdc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcOrder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcPart.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcProve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcQbf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcQuant.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcReconv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRefactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRenode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcReorder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRestruct.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcResub.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRewrite.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcRr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcStrash.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSweep.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcTiming.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcUnate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcUnreach.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcVerify.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abci\abcXsim.c
+# End Source File
+# End Group
+# Begin Group "cmd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdAlias.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdFlag.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdHist.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\cmd\cmdUtils.c
+# End Source File
+# End Group
+# Begin Group "io"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\io\io.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\io.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadAiger.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBaf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBlifAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadBlifMv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEdif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadPla.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioReadVerilog.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteAiger.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBaf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBench.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBlif.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteBlifMv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteDot.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteGml.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWritePla.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\io\ioWriteVerilog.c
+# End Source File
+# End Group
+# Begin Group "main"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\main\libSupport.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\main.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\main.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainFrame.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\main\mainUtils.c
+# End Source File
+# End Group
+# Begin Group "ver"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\ver\ver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\ver\verCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\ver\verFormula.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\ver\verParse.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\ver\verStream.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "bdd"
+
+# PROP Default_Filter ""
+# Begin Group "cudd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cudd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddApply.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddFind.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddInv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddNeg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAddWalsh.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAndAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAnneal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApa.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddAPI.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddApprox.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddAbs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddCorr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBddIte.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddBridge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddClip.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddCompose.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddDecomp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddEssent.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExact.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddExport.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenCof.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGenetic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddHarwell.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddInteract.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLCache.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLevelQ.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLinear.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddLiteral.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddMatMult.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddPriority.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddRef.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddReorder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSign.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSolve.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSplit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetHB.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSubsetSP.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddSymmetry.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddWindow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddCount.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddFuncs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddIsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddLin.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddPort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddReord.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSetop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cudd\cuddZddUtil.c
+# End Source File
+# End Group
+# Begin Group "epd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\epd\epd.h
+# End Source File
+# End Group
+# Begin Group "mtr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrBasic.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrGroup.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\mtr\mtrInt.h
+# End Source File
+# End Group
+# Begin Group "parse"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parse.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseEqn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\parse\parseStack.c
+# End Source File
+# End Group
+# Begin Group "dsd"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsd.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdLocal.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdProc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\dsd\dsdTree.c
+# End Source File
+# End Group
+# Begin Group "reo"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reo.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoProfile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSift.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoSwap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTest.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoTransfer.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\reo\reoUnits.c
+# End Source File
+# End Group
+# Begin Group "cas"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bdd\cas\cas.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cas\casCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bdd\cas\casDec.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "sat"
+
+# PROP Default_Filter ""
+# Begin Group "msat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msat.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatActivity.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClause.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatClauseVec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatOrderH.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatQueue.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverIo.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSolverSearch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\msat\msatVec.c
+# End Source File
+# End Group
+# Begin Group "fraig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigChoice.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigFeed.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigPrime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\fraig\fraigVec.c
+# End Source File
+# End Group
+# Begin Group "csat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\csat\csat_apis.h
+# End Source File
+# End Group
+# Begin Group "bsat"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satInter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satMem.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satStore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satStore.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satTrace.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satVec.h
+# End Source File
+# End Group
+# Begin Group "proof"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\proof\pr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\proof\pr.h
+# End Source File
+# End Group
+# End Group
+# Begin Group "opt"
+
+# PROP Default_Filter ""
+# Begin Group "fxu"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapD.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapS.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSelect.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSingle.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuUpdate.c
+# End Source File
+# End Group
+# Begin Group "rwr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrEva.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrExp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrTemp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\rwr\rwrUtil.c
+# End Source File
+# End Group
+# Begin Group "cut"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cut.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutExpand.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutList.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutMerge.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutNode.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutOracle.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutPre22.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\cut\cutTruth.c
+# End Source File
+# End Group
+# Begin Group "dec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\dec\dec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decAbc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decFactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\dec\decUtil.c
+# End Source File
+# End Group
+# Begin Group "sim"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\sim\sim.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSupp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSym.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simSymStr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sim\simUtils.c
+# End Source File
+# End Group
+# Begin Group "ret"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retArea.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retDelay.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retFlow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retIncrem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retLvalue.c
+# End Source File
+# End Group
+# Begin Group "res"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\res\res.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resDivs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resFilter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resStrash.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resWin.c
+# End Source File
+# End Group
+# Begin Group "lpk"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpk.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcMux.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMulti.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMux.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkSets.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "map"
+
+# PROP Default_Filter ""
+# Begin Group "fpga"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpga.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\fpga\fpgaVec.c
+# End Source File
+# End Group
+# Begin Group "mapper"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapper.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperCutUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperMatch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperRefs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSuper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperSwitch.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTree.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperUtils.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mapper\mapperVec.c
+# End Source File
+# End Group
+# Begin Group "mio"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mio.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioFunc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\mio\mioUtils.c
+# End Source File
+# End Group
+# Begin Group "super"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\super\super.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\super.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superAnd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superGate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\super\superWrite.c
+# End Source File
+# End Group
+# Begin Group "if"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\if\if.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifUtil.c
+# End Source File
+# End Group
+# End Group
+# Begin Group "misc"
+
+# PROP Default_Filter ""
+# Begin Group "extra"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extra.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddAuto.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddCas.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddKmap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddSymm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraBddUnate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilBitMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilFile.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMemory.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilMisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilProgress.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilReader.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\extra\extraUtilUtil.c
+# End Source File
+# End Group
+# Begin Group "st"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\st.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\st\stmm.h
+# End Source File
+# End Group
+# Begin Group "util"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\util\util_hack.h
+# End Source File
+# End Group
+# Begin Group "mvc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCompare.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcContain.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCover.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcCube.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivide.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcDivisor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcLits.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpAlg.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcOpBool.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcSort.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\mvc\mvcUtils.c
+# End Source File
+# End Group
+# Begin Group "vec"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vec.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecAtt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecFlt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecPtr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecStr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\vec\vecVec.h
+# End Source File
+# End Group
+# Begin Group "espresso"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cofactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cols.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\compl.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\contain.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cubehack.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cubestr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cvrin.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cvrm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cvrmisc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\cvrout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\dominate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\equiv.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\espresso.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\espresso.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\essen.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\exact.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\expand.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\gasp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\gimpel.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\globals.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\hack.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\indep.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\irred.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\map.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\matrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\mincov.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\mincov.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\mincov_int.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\opo.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\pair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\part.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\primes.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\reduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\rows.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\set.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\setc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\sharp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\sminterf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\solution.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\sparse.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\sparse.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\sparse_int.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\unate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\util_old.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\espresso\verify.c
+# End Source File
+# End Group
+# Begin Group "nm"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\nm\nm.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\nm\nmApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\nm\nmInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\nm\nmTable.c
+# End Source File
+# End Group
+# Begin Group "hash"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\hash\hash.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\hash\hashFlt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\hash\hashInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\hash\hashPtr.h
+# End Source File
+# End Group
+# End Group
+# Begin Group "ai"
+
+# PROP Default_Filter ""
+# Begin Group "hop"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hop.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\hop\hopUtil.c
+# End Source File
+# End Group
+# Begin Group "ivy"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivy.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyCanon.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyCutTrav.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyFastMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyFraig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyHaig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyMulti.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyResyn.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyRwr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivySeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyShow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ivy\ivyUtil.c
+# End Source File
+# End Group
+# Begin Group "rwt"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\rwt\rwt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\rwt\rwtDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\rwt\rwtMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\rwt\rwtUtil.c
+# End Source File
+# End Group
+# Begin Group "deco"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\deco\deco.h
+# End Source File
+# End Group
+# Begin Group "mem"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\mem\mem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\mem\mem.h
+# End Source File
+# End Group
+# Begin Group "ioa"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\ioa\ioa.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ioa\ioaReadAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ioa\ioaUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ioa\ioaWriteAig.c
+# End Source File
+# End Group
+# Begin Group "dar"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\dar\dar.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darBalance.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darData.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darPrec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darRefact.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darResub.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\dar\darScript.c
+# End Source File
+# End Group
+# Begin Group "fra"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fra.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraBmc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraCec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraClass.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraImp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraInd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraLcr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraPart.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraSec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\fra\fraSim.c
+# End Source File
+# End Group
+# Begin Group "cnf"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnf.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfData.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfPost.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\cnf\cnfWrite.c
+# End Source File
+# End Group
+# Begin Group "csw"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\csw\csw.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswTable.c
+# End Source File
+# End Group
+# Begin Group "kit"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\kit\cloud.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\cloud.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kit.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitBdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitCloud.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitFactor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitGraph.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitHop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitIsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\kit\kitTruth.c
+# End Source File
+# End Group
+# Begin Group "bdc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bdc\bdc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bdc\bdcCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bdc\bdcDec.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bdc\bdcInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bdc\bdcTable.c
+# End Source File
+# End Group
+# Begin Group "aig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigCheck.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigDfs.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigFanout.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigMffc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigOper.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigOrder.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigPart.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigRepr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigRet.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigScl.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigSeq.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigShow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigTable.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigTiming.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigTsim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigWin.c
+# End Source File
+# End Group
+# Begin Group "bar"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bar\bar.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bar\bar.h
+# End Source File
+# End Group
+# End Group
+# End Group
+# Begin Group "Header Files"
+
+# PROP Default_Filter "h;hpp;hxx;hm;inl"
+# End Group
+# End Target
+# End Project
diff --git a/abclib.dsw b/abclib.dsw
new file mode 100644
index 00000000..260ade17
--- /dev/null
+++ b/abclib.dsw
@@ -0,0 +1,29 @@
+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abclib"=.\abclib.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+
diff --git a/abctestlib.dsp b/abctestlib.dsp
new file mode 100644
index 00000000..e901cbda
--- /dev/null
+++ b/abctestlib.dsp
@@ -0,0 +1,102 @@
+# Microsoft Developer Studio Project File - Name="abctestlib" - Package Owner=<4>
+# Microsoft Developer Studio Generated Build File, Format Version 6.00
+# ** DO NOT EDIT **
+
+# TARGTYPE "Win32 (x86) Console Application" 0x0103
+
+CFG=abctestlib - Win32 Debug
+!MESSAGE This is not a valid makefile. To build this project using NMAKE,
+!MESSAGE use the Export Makefile command and run
+!MESSAGE 
+!MESSAGE NMAKE /f "abctestlib.mak".
+!MESSAGE 
+!MESSAGE You can specify a configuration when running NMAKE
+!MESSAGE by defining the macro CFG on the command line. For example:
+!MESSAGE 
+!MESSAGE NMAKE /f "abctestlib.mak" CFG="abctestlib - Win32 Debug"
+!MESSAGE 
+!MESSAGE Possible choices for configuration are:
+!MESSAGE 
+!MESSAGE "abctestlib - Win32 Release" (based on "Win32 (x86) Console Application")
+!MESSAGE "abctestlib - Win32 Debug" (based on "Win32 (x86) Console Application")
+!MESSAGE 
+
+# Begin Project
+# PROP AllowPerConfigDependencies 0
+# PROP Scc_ProjName ""
+# PROP Scc_LocalPath ""
+CPP=cl.exe
+RSC=rc.exe
+
+!IF  "$(CFG)" == "abctestlib - Win32 Release"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 0
+# PROP BASE Output_Dir "Release"
+# PROP BASE Intermediate_Dir "Release"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 0
+# PROP Output_Dir "Release"
+# PROP Intermediate_Dir "Release"
+# PROP Ignore_Export_Lib 0
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
+# ADD BASE RSC /l 0x409 /d "NDEBUG"
+# ADD RSC /l 0x409 /d "NDEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LINK32=link.exe
+# ADD BASE LINK32 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 /machine:I386
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_release.lib /nologo /subsystem:console /machine:I386 /out:"_TEST/abctestlib.exe"
+
+!ELSEIF  "$(CFG)" == "abctestlib - Win32 Debug"
+
+# PROP BASE Use_MFC 0
+# PROP BASE Use_Debug_Libraries 1
+# PROP BASE Output_Dir "Debug"
+# PROP BASE Intermediate_Dir "Debug"
+# PROP BASE Target_Dir ""
+# PROP Use_MFC 0
+# PROP Use_Debug_Libraries 1
+# PROP Output_Dir "Debug"
+# PROP Intermediate_Dir "Debug"
+# PROP Ignore_Export_Lib 0
+# PROP Target_Dir ""
+# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /FR /YX /FD /GZ /c
+# ADD BASE RSC /l 0x409 /d "_DEBUG"
+# ADD RSC /l 0x409 /d "_DEBUG"
+BSC32=bscmake.exe
+# ADD BASE BSC32 /nologo
+# ADD BSC32 /nologo
+LINK32=link.exe
+# ADD BASE LINK32 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 /debug /machine:I386 /pdbtype:sept
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_debug.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abctestlib.exe" /pdbtype:sept
+
+!ENDIF 
+
+# Begin Target
+
+# Name "abctestlib - Win32 Release"
+# Name "abctestlib - Win32 Debug"
+# Begin Group "Source Files"
+
+# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
+# Begin Source File
+
+SOURCE=.\demo.c
+# End Source File
+# End Group
+# Begin Group "Header Files"
+
+# PROP Default_Filter "h;hpp;hxx;hm;inl"
+# End Group
+# Begin Group "Resource Files"
+
+# PROP Default_Filter "ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe"
+# End Group
+# End Target
+# End Project
diff --git a/abctestlib.dsw b/abctestlib.dsw
new file mode 100644
index 00000000..7ae6cac9
--- /dev/null
+++ b/abctestlib.dsw
@@ -0,0 +1,29 @@
+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+
diff --git a/readme b/readme
index 13bb8e15..93e6f89d 100644
--- a/readme
+++ b/readme
@@ -11,6 +11,10 @@ Modify Makefile to have -DLIN (for 32-bits) or -DLIN64 (for 64-bits)
 If compiling as a static library, it is necessary to uncomment
 #define _LIB in "src/abc/main/main.c"
 
+To compile with Microsoft Visual Studio higher than 6.0,
+remove ABC_CHECK_LEAKS from the preprocessor definitions
+for the debug version (Project->Settings->C/C++->Preprocessor Definitions)
+
 Several things to try if it does not compile on your platform:
 - Try running all code (not only Makefile and depends.sh) through dos2unix
 - Try the following actions:
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index b0f3b1fb..5f1f724f 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -66,7 +66,7 @@ struct Ntl_Man_t_
     char *             pName;          // the name of this design
     char *             pSpec;          // the name of input file
     Vec_Ptr_t *        vModels;        // the array of all models used to represent boxes
-    int                BoxTypes[15];   // the array of box types among the models
+    int                BoxTypes[32];   // the array of box types among the models
     // memory managers
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Aig_MmFlex_t *     pMemSops;       // memory for SOPs
@@ -225,6 +225,7 @@ static inline int         Ntl_BoxIsWhite( Ntl_Obj_t * p )         { assert( Ntl_
 static inline int         Ntl_BoxIsBlack( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite;   } 
 static inline int         Ntl_BoxIsComb( Ntl_Obj_t * p )          { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb;     } 
 static inline int         Ntl_BoxIsSeq( Ntl_Obj_t * p )           { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb;    } 
+static inline int         Ntl_BoxIsNoMerge( Ntl_Obj_t * p )       { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrNoMerge; } 
 
 static inline int         Ntl_ObjIsMapLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
 static inline int         Ntl_ObjIsMapRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 06a1a51c..dd481537 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -222,7 +222,7 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     printf( "inv/buf = %5d  ", Ntl_ModelLut1Num(pRoot) );
     printf( "box = %4d  ",     Ntl_ModelBoxNum(pRoot) );
     printf( "mod = %3d  ",     Vec_PtrSize(p->vModels) );
-    printf( "net = %d",       Ntl_ModelCountNets(pRoot) );
+    printf( "net = %d",        Ntl_ModelCountNets(pRoot) );
     printf( "\n" );
     fflush( stdout );
     assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
@@ -262,10 +262,11 @@ void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
     Ntl_Mod_t * pModel = pObj->pImplem;
     int Number = 0;
     assert( Ntl_ObjIsBox(pObj) );
-    Number |= (pModel->attrWhite << 0);
-    Number |= (pModel->attrBox   << 1);
-    Number |= (pModel->attrComb  << 2);
-    Number |= (pModel->attrKeep  << 3);
+    Number |= (pModel->attrWhite   << 0);
+    Number |= (pModel->attrBox     << 1);
+    Number |= (pModel->attrComb    << 2);
+    Number |= (pModel->attrKeep    << 3);
+    Number |= (pModel->attrNoMerge << 4);
     pModel->pMan->BoxTypes[Number]++;
 }
 
@@ -291,19 +292,20 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
     printf( "BOX STATISTICS:\n" );
     Ntl_ModelForEachBox( pModel, pObj, i )
         Ntl_ManSaveBoxType( pObj );
-    for ( i = 0; i < 15; i++ )
+    for ( i = 0; i < 32; i++ )
     {
         if ( !p->BoxTypes[i] )
             continue;
         printf( "%5d :", p->BoxTypes[i] );
-        printf( " %s", ((i & 1) > 0)? "white": "black" );
-        printf( " %s", ((i & 2) > 0)? "box  ": "logic" );
-        printf( " %s", ((i & 4) > 0)? "comb ": "seq  " );
-        printf( " %s", ((i & 8) > 0)? "keep ": "sweep" );
+        printf( " %s", ((i &  1) > 0)? "white   ": "black   " );
+        printf( " %s", ((i &  2) > 0)? "box     ": "logic   " );
+        printf( " %s", ((i &  4) > 0)? "comb    ": "seq     " );
+        printf( " %s", ((i &  8) > 0)? "keep    ": "sweep   " );
+        printf( " %s", ((i & 16) > 0)? "no_merge": "merge   " );
         printf( "\n" );
     }
     printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
-    for ( i = 0; i < 15; i++ )
+    for ( i = 0; i < 32; i++ )
         p->BoxTypes[i] = 0;
 }
 
@@ -366,6 +368,11 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    pModelNew->attrWhite   = pModelOld->attrWhite;
+    pModelNew->attrBox       = pModelOld->attrBox;
+    pModelNew->attrComb       = pModelOld->attrComb;
+    pModelNew->attrKeep       = pModelOld->attrKeep;
+    pModelNew->attrNoMerge = pModelOld->attrNoMerge;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
     {
         if ( Ntl_ObjIsNode(pObj) )
@@ -423,10 +430,11 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
-    pModelNew->attrWhite = pModelOld->attrWhite;
-    pModelNew->attrBox     = pModelOld->attrBox;
-    pModelNew->attrComb     = pModelOld->attrComb;
-    pModelNew->attrKeep     = pModelOld->attrKeep;
+    pModelNew->attrWhite   = pModelOld->attrWhite;
+    pModelNew->attrBox       = pModelOld->attrBox;
+    pModelNew->attrComb       = pModelOld->attrComb;
+    pModelNew->attrKeep       = pModelOld->attrKeep;
+    pModelNew->attrNoMerge = pModelOld->attrNoMerge;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
         pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
     Ntl_ModelForEachNet( pModelOld, pNet, i )
@@ -504,10 +512,11 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
     // create model
     sprintf( Name, "%s%d", "latch", Init );
     pModel = Ntl_ModelAlloc( pMan, Name );
-    pModel->attrWhite = 1;
-    pModel->attrBox   = 1;
-    pModel->attrComb  = 0;
-    pModel->attrKeep  = 0;
+    pModel->attrWhite   = 1;
+    pModel->attrBox     = 1;
+    pModel->attrComb    = 0;
+    pModel->attrKeep    = 0;
+    pModel->attrNoMerge = 0;
     // create primary input
     pObj = Ntl_ModelCreatePi( pModel );
     pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" );
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 6eb2cc95..30f972c8 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -878,14 +878,14 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
             p->pNtk->attrBox = 1;
         else if ( strcmp( pToken, "logic" ) == 0 )
             p->pNtk->attrBox = 0;
-        else if ( strcmp( pToken, "white" ) == 0 )
-            p->pNtk->attrWhite = 1;
         else if ( strcmp( pToken, "comb" ) == 0 )
             p->pNtk->attrComb = 1;
         else if ( strcmp( pToken, "seq" ) == 0 )
             p->pNtk->attrComb = 0;
         else if ( strcmp( pToken, "keep" ) == 0 )
             p->pNtk->attrKeep = 1;
+        else if ( strcmp( pToken, "sweep" ) == 0 )
+            p->pNtk->attrKeep = 0;
         else 
         {
             sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName );
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 623fa3a6..9c8d55ae 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -66,6 +66,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
 //        fprintf( pFile, " %s", pModel->attrKeep?  "keep" : "sweep" );
         fprintf( pFile, "\n" );
     }
+    if ( pModel->attrNoMerge )
+        fprintf( pFile, ".no_merge\n" );
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 08275ff3..4ae07063 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -85,7 +85,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index 527f372d..37eb3349 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -65,6 +65,8 @@ struct Saig_IntMan_t_
     int              timeTotal;
 };
 
+static int Saig_M144pPerformOneStep( Saig_IntMan_t * p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -331,6 +333,7 @@ sat_solver * Saig_DeriveSatSolver(
     sat_solver_store_mark_roots( pSat );
     // return clauses to the original state
     Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
     return pSat;
 }
 
@@ -727,6 +730,103 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
     free( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Check inductive containment.]
+
+  Description [Given interpolant I and transition relation T, here we
+  check that I(x) * T(x,y) => T(y). ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
+{
+    sat_solver * pSat;
+    Aig_Man_t * pInterOld = p->pInter;
+    Aig_Man_t * pInterNew = p->pInterNew;
+    Aig_Man_t * pTrans    = p->pAigTrans;
+    Cnf_Dat_t * pCnfOld   = p->pCnfInter;
+    Cnf_Dat_t * pCnfNew   = Cnf_Derive( p->pInterNew, 0 ); 
+    Cnf_Dat_t * pCnfTrans = p->pCnfAig;
+    Aig_Obj_t * pObj, * pObj2;
+    int status, i, Lits[2];
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars );
+
+    // interpolant
+    for ( i = 0; i < pCnfNew->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
+            assert( 0 );
+    }
+
+    // connector clauses
+    Cnf_DataLift( pCnfTrans, pCnfNew->nVars );
+    Aig_ManForEachPi( pInterNew, pObj, i )
+    {
+        pObj2 = Saig_ManLo( pTrans, i );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfTrans->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfTrans->pClauses[i], pCnfTrans->pClauses[i+1] ) )
+            assert( 0 );
+    }
+
+    // connector clauses
+    Cnf_DataLift( pCnfNew, pCnfNew->nVars + pCnfTrans->nVars );
+    Aig_ManForEachPi( pInterNew, pObj, i )
+    {
+        pObj2 = Saig_ManLi( pTrans, i );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+
+    // complement the last literal
+    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
+    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
+    // add clauses of B
+    for ( i = 0; i < pCnfNew->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // complement the last literal
+    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
+    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
+
+    // return clauses to the original state
+    Cnf_DataLift( pCnfTrans, -pCnfNew->nVars );
+    Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars );
+    Cnf_DataFree( pCnfNew );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    sat_solver_delete( pSat );
+    return status == l_False;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Interplates while the number of conflicts is not exceeded.]
@@ -738,7 +838,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUseIp, int fVerbose, int * pDepth )
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth )
 {
     Saig_IntMan_t * p;
     Aig_Man_t * pAigTemp;
@@ -809,17 +909,20 @@ p->timeCnf += clock() - clk;
         // iterate the interpolation procedure
         for ( i = 0; ; i++ )
         {
-            if ( p->nFrames + i >= 75 )
+            if ( p->nFrames + i >= nFramesMax )
             {
                 if ( fVerbose )
-                    printf( "Reached limit (%d) on the number of timeframes.\n", 75 );
+                    printf( "Reached limit (%d) on the number of timeframes.\n", nFramesMax );
                 p->timeTotal = clock() - clkTotal;
                 Saig_ManagerFree( p );
                 return -1;
             }
             // perform interplation
             clk = clock();
-            RetValue = Saig_PerformOneStep( p, fUseIp );
+            if ( fUseIp )
+                RetValue = Saig_M144pPerformOneStep( p );
+            else
+                RetValue = Saig_PerformOneStep( p, 0 );
             if ( fVerbose )
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
@@ -859,7 +962,10 @@ clk = clock();
 p->timeRwr += clock() - clk;
             // check containment of interpolants
 clk = clock();
-            Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
+            if ( fCheckInd )
+                Status = Saig_ManCheckInductiveContainment( p );
+            else
+                Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
 p->timeEqu += clock() - clk;
             if ( Status ) // contained
             {
@@ -897,6 +1003,232 @@ p->timeCnf += clock() - clk;
     return RetValue;
 }
 
+
+#include "m114p.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the SAT solver for one interpolation run.]
+
+  Description [pInter is the previous interpolant. pAig is one time frame.
+  pFrames is the unrolled time frames.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+M114p_Solver_t Saig_M144pDeriveSatSolver( 
+    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
+    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
+    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
+    Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
+{
+    M114p_Solver_t pSat;
+    Aig_Obj_t * pObj, * pObj2;
+    int i, Lits[2];
+
+    // sanity checks
+    assert( Aig_ManRegNum(pInter) == 0 );
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pFrames) == 0 );
+    assert( Aig_ManPoNum(pInter) == 1 );
+    assert( Aig_ManPoNum(pFrames) == 1 );
+    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+
+    // prepare CNFs
+    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
+
+    *pvMapRoots = Vec_IntAlloc( 10000 );
+    *pvMapVars = Vec_IntAlloc( 0 );
+    Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
+    for ( i = 0; i < pCnfFrames->nVars; i++ )
+        Vec_IntWriteEntry( *pvMapVars, i, -2 );
+
+    // start the solver
+    pSat = M114p_SolverNew( 1 );
+    M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+    // add clauses of A
+    // interpolant
+    for ( i = 0; i < pCnfInter->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pInter, pObj, i )
+    {
+        pObj2 = Saig_ManLo( pAig, i );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfAig->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pFrames, pObj, i )
+    {
+        if ( i == Aig_ManRegNum(pAig) )
+            break;
+//        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+        Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
+
+        pObj2 = Saig_ManLi( pAig, i );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // add clauses of B
+    for ( i = 0; i < pCnfFrames->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 1 );
+        if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // return clauses to the original state
+    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, iVar;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+    // process root clauses
+    p = Aig_ManStart( 10000 );
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+        {
+            pInter = Aig_ManConst0(p);
+            for ( k = 0; k < nLits; k++ )
+            {
+                iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
+                if ( iVar < 0 ) // var of A or B
+                    continue;
+                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
+                pInter = Aig_Or( p, pInter, pVar );
+            }
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 );
+            else // var of B or C
+                pInter = Aig_And( p, pInter, pInter2 );
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    Vec_PtrFree( vInters );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_M144pPerformOneStep( Saig_IntMan_t * p )
+{
+    M114p_Solver_t pSat;
+    Vec_Int_t * vMapRoots, * vMapVars;
+    int clk, status, RetValue;
+    assert( p->pInterNew == NULL );
+    // derive the SAT solver
+    pSat = Saig_M144pDeriveSatSolver( p->pInter, p->pCnfInter, 
+        p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, 
+        &vMapRoots, &vMapVars );
+    // solve the problem
+clk = clock();
+    status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
+    p->nConfCur = M114p_SolverGetConflictNum( pSat );
+p->timeSat += clock() - clk;
+    if ( status == 0 )
+    {
+        RetValue = 1;
+clk = clock();
+        p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars );
+p->timeInt += clock() - clk;
+    }
+    else if ( status == 1 )
+    {
+        RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+    }
+    M114p_SolverDelete( pSat );
+    Vec_IntFree( vMapRoots );
+    Vec_IntFree( vMapVars );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1aa2c82..cb3d2d86 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15343,12 +15343,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nBTLimit;
+    int nFramesMax;
     int fRewrite;
     int fTransLoop;
     int fUsePudlak;
+    int fCheckInd;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15356,12 +15358,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nBTLimit   = 20000;
+    nFramesMax = 40;
     fRewrite   = 0;
     fTransLoop = 1;
     fUsePudlak = 0;
+    fCheckInd  = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15376,6 +15380,17 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesMax < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -15385,6 +15400,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePudlak ^= 1;
             break;
+        case 'i':
+            fCheckInd ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -15414,16 +15432,18 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
+    fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a691a205..e47582e9 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth );
+    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 6f2e1d11..bfa91ddc 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -55,11 +55,9 @@ int main( int argc, char * argv[] )
     bool fBatch, fInitSource, fInitRead, fFinalWrite;
 
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     
 //    Npn_Experiment();
 //    Npn_Generate();
@@ -256,11 +254,9 @@ void Abc_Start()
 {
     Abc_Frame_t * pAbc;
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     // start the glocal frame
     pAbc = Abc_FrameGetGlobalFrame();
     // source the resource file
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index f45afcbe..d63ed5d3 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -43,7 +43,7 @@ extern "C" {
 
 // this include should be the first one in the list
 // it is used to catch memory leaks on Windows
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
 #include "leaks.h"
 #endif
 
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 03de79f1..4c19b5ee 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -50,7 +50,7 @@ typedef long long          sint64;
 
 // this include should be the first one in the list
 // it is used to catch memory leaks on Windows
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
 #include "leaks.h"       
 #endif
 
diff --git a/src/misc/zlib/1.c b/src/misc/zlib/1.c
deleted file mode 100644
index 8a06a346..00000000
--- a/src/misc/zlib/1.c
+++ /dev/null
@@ -1,35 +0,0 @@
- Volume in drive C is IBM_PRELOAD
- Volume Serial Number is 20EA-F780
-
- Directory of C:\_projects\abc\src\misc\zlib
-
-07/02/2008  03:51 PM    <DIR>          .
-07/02/2008  03:51 PM    <DIR>          ..
-07/02/2008  03:51 PM                 0 1.c
-12/21/2004  04:52 PM             4,708 adler32.c
-06/02/2003  06:16 AM             9,545 algorithm.txt
-07/07/2003  07:37 AM             2,568 compress_.c
-06/13/2005  01:56 AM            13,616 crc32.c
-01/05/2003  04:53 PM            31,009 crc32.h
-07/18/2005  04:27 AM            65,899 deflate.c
-05/29/2005  05:55 PM            12,445 deflate.h
-07/11/2005  10:31 PM            32,129 gzio.c
-05/31/2005  12:58 AM            22,787 infback.c
-11/13/2004  06:05 AM            12,886 inffast.c
-01/01/2003  05:46 PM               418 inffast.h
-11/24/2002  11:44 PM             6,437 inffixed.h
-06/14/2005  11:50 PM            50,345 inflate.c
-11/13/2004  05:38 AM             6,031 inflate.h
-07/18/2005  04:27 AM            14,085 inftrees.c
-07/11/2005  08:50 AM             2,428 inftrees.h
-07/02/2008  02:52 PM                34 link.txt
-07/18/2005  04:25 AM             5,821 README
-06/13/2005  02:34 AM            45,246 trees.c
-02/24/1998  12:14 PM             8,572 trees.h
-07/07/2003  07:36 AM             2,148 uncompr.c
-05/28/2005  08:40 AM             9,876 zconf.h
-07/18/2005  04:26 AM            67,545 zlib.h
-06/13/2005  02:37 AM             7,454 zutil.c
-07/11/2005  10:35 PM             7,128 zutil.h
-              26 File(s)        441,160 bytes
-               2 Dir(s)   1,641,279,488 bytes free
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index cc780580..5837e68f 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -941,7 +941,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     // stop the proof
     if ( p->fProofWrite )
-    {
+    { 
         fclose( p->pFile );
         p->pFile = NULL;    
     }
diff --git a/src/sat/psat/m114p.h b/src/sat/psat/m114p.h
new file mode 100644
index 00000000..5050cb4b
--- /dev/null
+++ b/src/sat/psat/m114p.h
@@ -0,0 +1,39 @@
+// C-language header for MiniSat 1.14p
+
+#ifndef m114p_h
+#define m114p_h
+
+#include "m114p_types.h"
+
+// SAT solver APIs
+extern M114p_Solver_t M114p_SolverNew( int fRecordProof );
+extern void           M114p_SolverDelete( M114p_Solver_t s );
+extern void           M114p_SolverPrintStats( M114p_Solver_t s, double Time );
+extern void           M114p_SolverSetVarNum( M114p_Solver_t s, int nVars );
+extern int            M114p_SolverAddClause( M114p_Solver_t s, lit* begin, lit* end );
+extern int            M114p_SolverSimplify( M114p_Solver_t s );
+extern int            M114p_SolverSolve( M114p_Solver_t s, lit* begin, lit* end, int nConfLimit );
+extern int            M114p_SolverGetConflictNum( M114p_Solver_t s );
+
+// proof status APIs
+extern int            M114p_SolverProofIsReady( M114p_Solver_t s );
+extern void           M114p_SolverProofSave( M114p_Solver_t s, char * pFileName );
+extern int            M114p_SolverProofClauseNum( M114p_Solver_t s );
+
+// proof traversal APIs
+extern int            M114p_SolverGetFirstRoot( M114p_Solver_t s, int ** ppLits );
+extern int            M114p_SolverGetNextRoot( M114p_Solver_t s, int ** ppLits );
+extern int            M114p_SolverGetFirstChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars );
+extern int            M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars );
+
+// iterator over the root clauses (should be called first)
+#define M114p_SolverForEachRoot( s, ppLits, nLits, i )                           \
+    for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits;             \
+          i++, nLits = M114p_SolverGetNextRoot(s, ppLits) )
+
+// iterator over the learned clauses (should be called after iterating over roots)
+#define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i )               \
+    for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \
+          i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) )
+
+#endif
\ No newline at end of file
diff --git a/src/sat/psat/m114p_types.h b/src/sat/psat/m114p_types.h
new file mode 100644
index 00000000..54a20c5c
--- /dev/null
+++ b/src/sat/psat/m114p_types.h
@@ -0,0 +1,9 @@
+// C-language header for MiniSat 1.14p
+
+#ifndef m114p_types_h
+#define m114p_types_h
+
+typedef int   M114p_Solver_t;
+typedef int   lit;
+
+#endif
\ No newline at end of file
diff --git a/src/sat/psat/module.make b/src/sat/psat/module.make
new file mode 100644
index 00000000..d6d908e7
--- /dev/null
+++ b/src/sat/psat/module.make
@@ -0,0 +1 @@
+SRC +=