diff --git a/src/proof/bbr/bbr.h b/src/bdd/bbr/bbr.h
similarity index 100%
rename from src/proof/bbr/bbr.h
rename to src/bdd/bbr/bbr.h
diff --git a/src/proof/bbr/bbrCex.c b/src/bdd/bbr/bbrCex.c
similarity index 100%
rename from src/proof/bbr/bbrCex.c
rename to src/bdd/bbr/bbrCex.c
diff --git a/src/proof/bbr/bbrImage.c b/src/bdd/bbr/bbrImage.c
similarity index 100%
rename from src/proof/bbr/bbrImage.c
rename to src/bdd/bbr/bbrImage.c
diff --git a/src/proof/bbr/bbrNtbdd.c b/src/bdd/bbr/bbrNtbdd.c
similarity index 100%
rename from src/proof/bbr/bbrNtbdd.c
rename to src/bdd/bbr/bbrNtbdd.c
diff --git a/src/proof/bbr/bbrReach.c b/src/bdd/bbr/bbrReach.c
similarity index 100%
rename from src/proof/bbr/bbrReach.c
rename to src/bdd/bbr/bbrReach.c
diff --git a/src/proof/bbr/bbr_.c b/src/bdd/bbr/bbr_.c
similarity index 100%
rename from src/proof/bbr/bbr_.c
rename to src/bdd/bbr/bbr_.c
diff --git a/src/bdd/bbr/module.make b/src/bdd/bbr/module.make
new file mode 100644
index 000000000..4bb1a2927
--- /dev/null
+++ b/src/bdd/bbr/module.make
@@ -0,0 +1,4 @@
+SRC +=    src/bdd/bbr/bbrCex.c \
+    src/bdd/bbr/bbrImage.c \
+    src/bdd/bbr/bbrNtbdd.c \
+    src/bdd/bbr/bbrReach.c
diff --git a/src/misc/extra/extraBdd.h b/src/bdd/extrab/extraBdd.h
similarity index 100%
rename from src/misc/extra/extraBdd.h
rename to src/bdd/extrab/extraBdd.h
diff --git a/src/misc/extra/extraBddAuto.c b/src/bdd/extrab/extraBddAuto.c
similarity index 100%
rename from src/misc/extra/extraBddAuto.c
rename to src/bdd/extrab/extraBddAuto.c
diff --git a/src/misc/extra/extraBddCas.c b/src/bdd/extrab/extraBddCas.c
similarity index 100%
rename from src/misc/extra/extraBddCas.c
rename to src/bdd/extrab/extraBddCas.c
diff --git a/src/misc/extra/extraBddImage.c b/src/bdd/extrab/extraBddImage.c
similarity index 100%
rename from src/misc/extra/extraBddImage.c
rename to src/bdd/extrab/extraBddImage.c
diff --git a/src/misc/extra/extraBddKmap.c b/src/bdd/extrab/extraBddKmap.c
similarity index 100%
rename from src/misc/extra/extraBddKmap.c
rename to src/bdd/extrab/extraBddKmap.c
diff --git a/src/misc/extra/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c
similarity index 100%
rename from src/misc/extra/extraBddMisc.c
rename to src/bdd/extrab/extraBddMisc.c
diff --git a/src/misc/extra/extraBddSymm.c b/src/bdd/extrab/extraBddSymm.c
similarity index 100%
rename from src/misc/extra/extraBddSymm.c
rename to src/bdd/extrab/extraBddSymm.c
diff --git a/src/misc/extra/extraBddTime.c b/src/bdd/extrab/extraBddTime.c
similarity index 100%
rename from src/misc/extra/extraBddTime.c
rename to src/bdd/extrab/extraBddTime.c
diff --git a/src/misc/extra/extraBddUnate.c b/src/bdd/extrab/extraBddUnate.c
similarity index 100%
rename from src/misc/extra/extraBddUnate.c
rename to src/bdd/extrab/extraBddUnate.c
diff --git a/src/bdd/extrab/module.make b/src/bdd/extrab/module.make
new file mode 100644
index 000000000..38cdddb6a
--- /dev/null
+++ b/src/bdd/extrab/module.make
@@ -0,0 +1,8 @@
+SRC +=    src/bdd/extrab/extraBddAuto.c \
+    src/bdd/extrab/extraBddCas.c \
+    src/bdd/extrab/extraBddImage.c \
+    src/bdd/extrab/extraBddKmap.c \
+    src/bdd/extrab/extraBddMisc.c \
+    src/bdd/extrab/extraBddSymm.c \
+    src/bdd/extrab/extraBddTime.c \
+    src/bdd/extrab/extraBddUnate.c
diff --git a/src/proof/llb/llb.c b/src/bdd/llb/llb.c
similarity index 100%
rename from src/proof/llb/llb.c
rename to src/bdd/llb/llb.c
diff --git a/src/proof/llb/llb.h b/src/bdd/llb/llb.h
similarity index 100%
rename from src/proof/llb/llb.h
rename to src/bdd/llb/llb.h
diff --git a/src/proof/llb/llb1Cluster.c b/src/bdd/llb/llb1Cluster.c
similarity index 100%
rename from src/proof/llb/llb1Cluster.c
rename to src/bdd/llb/llb1Cluster.c
diff --git a/src/proof/llb/llb1Constr.c b/src/bdd/llb/llb1Constr.c
similarity index 100%
rename from src/proof/llb/llb1Constr.c
rename to src/bdd/llb/llb1Constr.c
diff --git a/src/proof/llb/llb1Core.c b/src/bdd/llb/llb1Core.c
similarity index 100%
rename from src/proof/llb/llb1Core.c
rename to src/bdd/llb/llb1Core.c
diff --git a/src/proof/llb/llb1Group.c b/src/bdd/llb/llb1Group.c
similarity index 100%
rename from src/proof/llb/llb1Group.c
rename to src/bdd/llb/llb1Group.c
diff --git a/src/proof/llb/llb1Hint.c b/src/bdd/llb/llb1Hint.c
similarity index 100%
rename from src/proof/llb/llb1Hint.c
rename to src/bdd/llb/llb1Hint.c
diff --git a/src/proof/llb/llb1Man.c b/src/bdd/llb/llb1Man.c
similarity index 100%
rename from src/proof/llb/llb1Man.c
rename to src/bdd/llb/llb1Man.c
diff --git a/src/proof/llb/llb1Matrix.c b/src/bdd/llb/llb1Matrix.c
similarity index 100%
rename from src/proof/llb/llb1Matrix.c
rename to src/bdd/llb/llb1Matrix.c
diff --git a/src/proof/llb/llb1Pivot.c b/src/bdd/llb/llb1Pivot.c
similarity index 100%
rename from src/proof/llb/llb1Pivot.c
rename to src/bdd/llb/llb1Pivot.c
diff --git a/src/proof/llb/llb1Reach.c b/src/bdd/llb/llb1Reach.c
similarity index 100%
rename from src/proof/llb/llb1Reach.c
rename to src/bdd/llb/llb1Reach.c
diff --git a/src/proof/llb/llb1Sched.c b/src/bdd/llb/llb1Sched.c
similarity index 100%
rename from src/proof/llb/llb1Sched.c
rename to src/bdd/llb/llb1Sched.c
diff --git a/src/proof/llb/llb2Bad.c b/src/bdd/llb/llb2Bad.c
similarity index 100%
rename from src/proof/llb/llb2Bad.c
rename to src/bdd/llb/llb2Bad.c
diff --git a/src/proof/llb/llb2Core.c b/src/bdd/llb/llb2Core.c
similarity index 100%
rename from src/proof/llb/llb2Core.c
rename to src/bdd/llb/llb2Core.c
diff --git a/src/proof/llb/llb2Driver.c b/src/bdd/llb/llb2Driver.c
similarity index 100%
rename from src/proof/llb/llb2Driver.c
rename to src/bdd/llb/llb2Driver.c
diff --git a/src/proof/llb/llb2Dump.c b/src/bdd/llb/llb2Dump.c
similarity index 100%
rename from src/proof/llb/llb2Dump.c
rename to src/bdd/llb/llb2Dump.c
diff --git a/src/proof/llb/llb2Flow.c b/src/bdd/llb/llb2Flow.c
similarity index 100%
rename from src/proof/llb/llb2Flow.c
rename to src/bdd/llb/llb2Flow.c
diff --git a/src/proof/llb/llb2Image.c b/src/bdd/llb/llb2Image.c
similarity index 100%
rename from src/proof/llb/llb2Image.c
rename to src/bdd/llb/llb2Image.c
diff --git a/src/proof/llb/llb3Image.c b/src/bdd/llb/llb3Image.c
similarity index 100%
rename from src/proof/llb/llb3Image.c
rename to src/bdd/llb/llb3Image.c
diff --git a/src/proof/llb/llb3Nonlin.c b/src/bdd/llb/llb3Nonlin.c
similarity index 100%
rename from src/proof/llb/llb3Nonlin.c
rename to src/bdd/llb/llb3Nonlin.c
diff --git a/src/proof/llb/llb4Cex.c b/src/bdd/llb/llb4Cex.c
similarity index 100%
rename from src/proof/llb/llb4Cex.c
rename to src/bdd/llb/llb4Cex.c
diff --git a/src/proof/llb/llb4Cluster.c b/src/bdd/llb/llb4Cluster.c
similarity index 100%
rename from src/proof/llb/llb4Cluster.c
rename to src/bdd/llb/llb4Cluster.c
diff --git a/src/proof/llb/llb4Image.c b/src/bdd/llb/llb4Image.c
similarity index 100%
rename from src/proof/llb/llb4Image.c
rename to src/bdd/llb/llb4Image.c
diff --git a/src/proof/llb/llb4Map.c b/src/bdd/llb/llb4Map.c
similarity index 100%
rename from src/proof/llb/llb4Map.c
rename to src/bdd/llb/llb4Map.c
diff --git a/src/proof/llb/llb4Nonlin.c b/src/bdd/llb/llb4Nonlin.c
similarity index 100%
rename from src/proof/llb/llb4Nonlin.c
rename to src/bdd/llb/llb4Nonlin.c
diff --git a/src/proof/llb/llb4Sweep.c b/src/bdd/llb/llb4Sweep.c
similarity index 100%
rename from src/proof/llb/llb4Sweep.c
rename to src/bdd/llb/llb4Sweep.c
diff --git a/src/proof/llb/llbInt.h b/src/bdd/llb/llbInt.h
similarity index 99%
rename from src/proof/llb/llbInt.h
rename to src/bdd/llb/llbInt.h
index e2afe59a5..238da04ed 100644
--- a/src/proof/llb/llbInt.h
+++ b/src/bdd/llb/llbInt.h
@@ -32,7 +32,7 @@
 #include "proof/ssw/ssw.h"
 #include "llb.h"
 
-#include "misc/extra/extraBdd.h"
+#include "bdd/extrab/extraBdd.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/bdd/llb/module.make b/src/bdd/llb/module.make
new file mode 100644
index 000000000..6d253d502
--- /dev/null
+++ b/src/bdd/llb/module.make
@@ -0,0 +1,22 @@
+SRC +=    src/bdd/llb/llb1Cluster.c \
+    src/bdd/llb/llb1Constr.c \
+    src/bdd/llb/llb1Core.c \
+    src/bdd/llb/llb1Group.c \
+    src/bdd/llb/llb1Hint.c \
+    src/bdd/llb/llb1Man.c \
+    src/bdd/llb/llb1Matrix.c \
+    src/bdd/llb/llb1Pivot.c \
+    src/bdd/llb/llb1Reach.c \
+    src/bdd/llb/llb1Sched.c \
+    src/bdd/llb/llb2Bad.c \
+    src/bdd/llb/llb2Core.c \
+    src/bdd/llb/llb2Driver.c \
+    src/bdd/llb/llb2Dump.c \
+    src/bdd/llb/llb2Flow.c \
+    src/bdd/llb/llb2Image.c \
+    src/bdd/llb/llb3Image.c \
+    src/bdd/llb/llb3Nonlin.c \
+    src/bdd/llb/llb4Cex.c \
+    src/bdd/llb/llb4Image.c \
+    src/bdd/llb/llb4Nonlin.c \
+    src/bdd/llb/llb4Sweep.c
diff --git a/src/bdd/parse/module.make b/src/bdd/parse/module.make
deleted file mode 100644
index 4f590f019..000000000
--- a/src/bdd/parse/module.make
+++ /dev/null
@@ -1,3 +0,0 @@
-SRC +=  src/bdd/parse/parseCore.c \
-    src/bdd/parse/parseEqn.c \
-    src/bdd/parse/parseStack.c
diff --git a/src/misc/parse/module.make b/src/misc/parse/module.make
new file mode 100644
index 000000000..bb13c8e5e
--- /dev/null
+++ b/src/misc/parse/module.make
@@ -0,0 +1,2 @@
+SRC +=  src/misc/parse/parseEqn.c \
+    src/misc/parse/parseStack.c
diff --git a/src/bdd/parse/parse.h b/src/misc/parse/parse.h
similarity index 100%
rename from src/bdd/parse/parse.h
rename to src/misc/parse/parse.h
diff --git a/src/bdd/parse/parseCore.c b/src/misc/parse/parseCore.c
similarity index 100%
rename from src/bdd/parse/parseCore.c
rename to src/misc/parse/parseCore.c
diff --git a/src/bdd/parse/parseEqn.c b/src/misc/parse/parseEqn.c
similarity index 99%
rename from src/bdd/parse/parseEqn.c
rename to src/misc/parse/parseEqn.c
index ac32e528b..eef95dc28 100644
--- a/src/bdd/parse/parseEqn.c
+++ b/src/misc/parse/parseEqn.c
@@ -16,14 +16,11 @@
 
 ***********************************************************************/
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 #include "parseInt.h"
-#include "misc/vec/vec.h"
-#include "aig/hop/hop.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/bdd/parse/parseInt.h b/src/misc/parse/parseInt.h
similarity index 97%
rename from src/bdd/parse/parseInt.h
rename to src/misc/parse/parseInt.h
index 80ed945a1..42a9805b8 100644
--- a/src/bdd/parse/parseInt.h
+++ b/src/misc/parse/parseInt.h
@@ -24,10 +24,8 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
-#include <stdio.h>
-#include "misc/extra/extraBdd.h"
-#include "parse.h"
+#include "aig/hop/hop.h"
+#include "misc/vec/vec.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/bdd/parse/parseStack.c b/src/misc/parse/parseStack.c
similarity index 100%
rename from src/bdd/parse/parseStack.c
rename to src/misc/parse/parseStack.c
diff --git a/src/proof/bbr/module.make b/src/proof/bbr/module.make
deleted file mode 100644
index 11ba768e3..000000000
--- a/src/proof/bbr/module.make
+++ /dev/null
@@ -1,4 +0,0 @@
-SRC +=    src/proof/bbr/bbrCex.c \
-    src/proof/bbr/bbrImage.c \
-    src/proof/bbr/bbrNtbdd.c \
-    src/proof/bbr/bbrReach.c
diff --git a/src/proof/llb/module.make b/src/proof/llb/module.make
deleted file mode 100644
index b08c42afc..000000000
--- a/src/proof/llb/module.make
+++ /dev/null
@@ -1,22 +0,0 @@
-SRC +=    src/proof/llb/llb1Cluster.c \
-    src/proof/llb/llb1Constr.c \
-    src/proof/llb/llb1Core.c \
-    src/proof/llb/llb1Group.c \
-    src/proof/llb/llb1Hint.c \
-    src/proof/llb/llb1Man.c \
-    src/proof/llb/llb1Matrix.c \
-    src/proof/llb/llb1Pivot.c \
-    src/proof/llb/llb1Reach.c \
-    src/proof/llb/llb1Sched.c \
-    src/proof/llb/llb2Bad.c \
-    src/proof/llb/llb2Core.c \
-    src/proof/llb/llb2Driver.c \
-    src/proof/llb/llb2Dump.c \
-    src/proof/llb/llb2Flow.c \
-    src/proof/llb/llb2Image.c \
-    src/proof/llb/llb3Image.c \
-    src/proof/llb/llb3Nonlin.c \
-    src/proof/llb/llb4Cex.c \
-    src/proof/llb/llb4Image.c \
-    src/proof/llb/llb4Nonlin.c \
-    src/proof/llb/llb4Sweep.c