diff --git a/src/dpa/Makefile b/src/dpa/Makefile
index ae529cc..36585ea 100644
--- a/src/dpa/Makefile
+++ b/src/dpa/Makefile
@@ -2,7 +2,7 @@ include ../makefile.include
 
 ifeq ($(STATIC_DPA), 1)
   CXX += -static-libstdc++ -static-libgcc -static
-  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
+#  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
   LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
 else
   LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
diff --git a/src/makefile.include b/src/makefile.include
index edd40be..5d0773f 100644
--- a/src/makefile.include
+++ b/src/makefile.include
@@ -50,7 +50,8 @@ endif
 GPP=g++ -std=c++17
 
 ####	flags
-CFLAG_OPT = -g -O3
+#CFLAG_OPT = -g -O3
+CFLAG_OPT = -O3
 
 #### includes
 INCLUDE_DIRS = 
@@ -59,7 +60,8 @@ CFLAGS_INC = $(INCLUDE_DIRS)
 CFLAGS = -c $(CFLAGS_INC) $(CFLAG_OPT)
 
 #### optional flags
-FLAG_PG = -pg
+#FLAG_PG = -pg
+FLAG_PG = 
 
 #### link flags
 LINK_FLAGS = $(CFLAG_OPT)
diff --git a/src/reach/Makefile b/src/reach/Makefile
index 3665bae..205677e 100644
--- a/src/reach/Makefile
+++ b/src/reach/Makefile
@@ -1,10 +1,10 @@
 include ../makefile.include
 
-CFLAGS += -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label
+CFLAGS += -fPIC -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label
 
 ifeq ($(STATIC_REA), 1)
   CXX += -static-libstdc++ -static-libgcc -static
-  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
+#  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
   LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
 else
   LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
@@ -12,7 +12,7 @@ endif
 
 ifeq ($(ENABLE_Y2), 1)
 	Y2_DIR = $(DEPS)/yices2
-	Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a
+	Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a  $(STATIC_GMPXX) $(STATIC_GMP)
 	INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include
 	LINKLIBS += $(Y2_LIB)
 	CFLAGS += -D_Y2
@@ -38,11 +38,15 @@ endif
 
 ifeq ($(ENABLE_M5), 1)
 	MSAT_DIR = $(DEPS)/mathsat
-	MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP)
+	MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP)
 	INCLUDE += -I$(MSAT_DIR)/include
 	LINKLIBS += $(MSAT_LIB)
 	CFLAGS += -D_M5
 endif
+ifeq ($(CONFIG_M5), 1)
+  CFLAGS += -DBACKEND_M5
+  REACH_SUFFIX = m5
+endif
 
 ifeq ($(ENABLE_Z3), 1)
   Z3_DIR = $(DEPS)/z3
diff --git a/src/reach/reach_backend.h b/src/reach/reach_backend.h
index b47853c..1fedbee 100644
--- a/src/reach/reach_backend.h
+++ b/src/reach/reach_backend.h
@@ -26,11 +26,23 @@
 /// Configurations
 /// Note: Only one of the below flag should be enabled
 
+// #define BACKEND_Y2BT	// Yices 2 for abstract, Boolector for bv queries
 // #define BACKEND_Y2		// Yices 2 for all queries
 // #define BACKEND_BT		// Boolector for all queries
-// #define BACKEND_Y2BT	// Yices 2 for abstract, Boolector for bv queries
+// #define BACKEND_MT		// MathSAT 5 for all queries
+
 
-// Use Y2 backend for all abstract queries
+/// Config: BACKEND_Y2BT
+#ifdef BACKEND_Y2BT
+	#define SOLVER_CTI		  y2_API		// Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
+	#define SOLVER_REACH	  y2_API		// Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
+	#define SOLVER_CONTAIN	  y2_API		// Solver for checking if frame restriction global
+	#define SOLVER_AB		  y2_API		// Solver for all other abstract queries: Basis check, Lemma redundancy check
+	#define SOLVER_CORE       y2_API		// Solver for getting unsat core
+	#define SOLVER_MUS		  y2_API		// Solver for getting minimal unsat core
+
+	#define SOLVER_BV         bt_API	// Solver for concrete / bit-vector queries
+#endif
 
 /// Config: BACKEND_Y2
 #ifdef BACKEND_Y2
@@ -56,16 +68,16 @@
 	#define SOLVER_BV         bt_API	// Solver for concrete / bit-vector queries
 #endif
 
-/// Config: BACKEND_Y2BT
-#ifdef BACKEND_Y2BT
-	#define SOLVER_CTI		  y2_API		// Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
-	#define SOLVER_REACH	  y2_API		// Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
-	#define SOLVER_CONTAIN	  y2_API		// Solver for checking if frame restriction global
-	#define SOLVER_AB		  y2_API		// Solver for all other abstract queries: Basis check, Lemma redundancy check
-	#define SOLVER_CORE       y2_API		// Solver for getting unsat core
-	#define SOLVER_MUS		  y2_API		// Solver for getting minimal unsat core
+/// Config: BACKEND_M5
+#ifdef BACKEND_M5
+	#define SOLVER_CTI		  m5_API		// Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
+	#define SOLVER_REACH	  m5_API		// Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
+	#define SOLVER_CONTAIN	  m5_API		// Solver for checking if frame restriction global
+	#define SOLVER_AB		  m5_API		// Solver for all other abstract queries: Basis check, Lemma redundancy check
+	#define SOLVER_CORE       m5_API		// Solver for getting unsat core
+	#define SOLVER_MUS		  m5_API		// Solver for getting minimal unsat core
 
-	#define SOLVER_BV         bt_API	// Solver for concrete / bit-vector queries
+	#define SOLVER_BV         m5_API	// Solver for concrete / bit-vector queries
 #endif
 
 
diff --git a/src/vwn/Makefile b/src/vwn/Makefile
index 130487c..4b0077a 100644
--- a/src/vwn/Makefile
+++ b/src/vwn/Makefile
@@ -8,7 +8,7 @@ LINKLIBS =
 
 ifeq ($(STATIC_VWN), 1)
   CXX += -static-libstdc++ -static-libgcc -static
-  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
+#  LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
   LINK_FLAGS += -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
   LINKLIBS += $(STATIC_GMPXX) $(STATIC_GMP)
 else
diff --git a/workers.txt b/workers.txt
index 4a72072..b6b78eb 100755
--- a/workers.txt
+++ b/workers.txt
@@ -1,16 +1,16 @@
-python3 avr.py --split
+python3 avr.py --backend y2 --split
 python3 avr.py --kind --abstract sa --backend bt
-python3 avr.py --kind --abstract sa --split
-python3 avr.py --abstract sa --backend bt
+python3 avr.py --kind --abstract sa --backend y2 --split
 python3 avr.py --abstract sa
-python3 avr.py
 python3 avr.py --bmc --abstract sa --backend bt --split
-python3 avr.py --bmc --abstract sa+heavy
-python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
-python3 avr.py --abstract sa4 --split --forward 1 --interpol 1
-python3 avr.py --abstract sa+heavy --backend bt --split
+python3 avr.py
+python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1
+python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1
+python3 avr.py --split --level 0
+python3 avr.py --abstract sa8 --backend y2 --split --interpol 1
 python3 avr.py --kind --abstract sa --backend bt --split
-python3 avr.py --abstract sa8 --split --interpol 1
-python3 avr.py --abstract sa16 --split --forward 1 --backend bt
-python3 avr.py --abstract sa32 --backend bt --level 0 --granularity 3
-python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
+python3 avr.py --bmc --abstract sa --backend y2
+python3 avr.py --abstract sa --backend bt
+python3 avr.py --abstract sa+heavy
+python3 avr.py --bmc --abstract sa+heavy --backend bt
+python3 avr.py --kind --abstract sa+heavy --backend bt