diff --git a/.gitignore b/.gitignore
index 1ad555c..9a77152 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,11 +6,13 @@
 .idea/
 
 build/bin*/dpa
-build/bin*/reach
+build/bin*/reach*
 build/bin*/vwn
 
+hwmcc*/
 deps/*
 output/*
+xtras/*/
 
 *.a
 *.o
diff --git a/build/avr b/avr
similarity index 97%
rename from build/avr
rename to avr
index 2e4de29..7074eb4 100755
--- a/build/avr
+++ b/avr
@@ -35,6 +35,7 @@ enKind="${32}"
 bmcKmax="${33}"
 createAig="${34}"
 parseOnly="${35}"
+backendSuffix="${36}"
 
 BM_PATH="$p_dir"
 OUT_DIR="$p_out"
@@ -293,7 +294,7 @@ then
 	exit $avr_exit
 fi
 
-$p_bin/reach $OUT_PATH $p_bin > $OUT_PATH/data/reach.output 2>> >(tee -a $OUT_PATH/avr.err >&2)  & echo $! > $pidFile
+$p_bin/reach_${backendSuffix} $OUT_PATH $p_bin > $OUT_PATH/data/reach.output 2>> >(tee -a $OUT_PATH/avr.err >&2)  & echo $! > $pidFile
 wait
 avr_exit=$?
 
diff --git a/avr.py b/avr.py
index 7ccf689..0bf84ef 100755
--- a/avr.py
+++ b/avr.py
@@ -23,16 +23,17 @@
 
 DEFAULT_TOP="-"
 DEFAULT_BIN="build/bin"
+DEFAULT_BACKEND="y2"
 DEFAULT_NAME="test"
 DEFAULT_PROP_SELECT="-"
 DEFAULT_INIT_FILE="-"
 DEFAULT_OUT="output"
 DEFAULT_YOSYS="deps/yosys"
 DEFAULT_CLK="clk"
-DEFAULT_TIMEOUT=3600
-DEFAULT_MEMOUT=64000
+DEFAULT_TIMEOUT=3590
+DEFAULT_MEMOUT=118000
 DEFAULT_MEMORY=False
-DEFAULT_SPLIT=True
+DEFAULT_SPLIT=False
 DEFAULT_GRANULARITY=2
 DEFAULT_RANDOM=False
 DEFAULT_EFFORT_MININV=0
@@ -64,6 +65,7 @@ def getopts(header):
 	p.add_argument('-n', '--name',      help='<test-name> (default: %s)' % DEFAULT_NAME, type=str, default=DEFAULT_NAME)
 	p.add_argument('-o', '--out',       help='<output-path> (default: %s)' % DEFAULT_OUT, type=str, default=DEFAULT_OUT)
 	p.add_argument('-b', '--bin',       help='binary path (default: %s)' % DEFAULT_BIN, type=str, default=DEFAULT_BIN)
+	p.add_argument('--backend',         help='backend to use: y2, bt, m5 (default: %s)' % DEFAULT_BACKEND, type=str, default=DEFAULT_BACKEND)
 	p.add_argument('-y', '--yosys',     help='path to yosys installation (default: %s)' % DEFAULT_YOSYS, type=str, default=DEFAULT_YOSYS)
 	p.add_argument('--vmt',             help='toggles using vmt frontend (default: %s)' % DEFAULT_EN_VMT, action="count", default=0)
 	p.add_argument('-j', '--jg',        help='toggles using jg frontend (default: %s)' % DEFAULT_EN_JG, action="count", default=0)
@@ -123,14 +125,14 @@ def split_path(name):
 def main():
 	known, opts = getopts(header)
 	print(short_header)
-	if not os.path.isfile("build/avr"):
+	if not os.path.isfile("avr"):
 		raise Exception("avr: main shell script not found")
 	if not os.path.isfile(opts.bin + "/vwn"):
-		raise Exception("avr: vwn binary not found")
+		raise Exception(f"avr: vwn binary not found in {opts.bin}")
 	if not os.path.isfile(opts.bin + "/dpa"):
-		raise Exception("avr: dpa binary not found")
-	if not os.path.isfile(opts.bin + "/reach"):
-		raise Exception("avr: reach binary not found")
+		raise Exception(f"avr: dpa binary not found in {opts.bin}")
+	if not os.path.isfile(opts.bin + "/reach_" + opts.backend):
+		raise Exception(f"avr: reach binary not found in {opts.bin}")
 	if not os.path.exists(opts.out):
 		os.makedirs(opts.out)
 
@@ -161,6 +163,8 @@ def main():
 			en_bt = not DEFAULT_EN_BTOR2
 		
 	print("\t(output dir: %s/work_%s)" % (opts.out, opts.name))
+	print("\t(backend: %s)" % opts.backend)
+
 	if (en_jg):
 		print("\t(frontend: jg)")
 		en_vmt = False
@@ -185,7 +189,7 @@ def main():
 				opts.yosys = ys_path
 			print("\t(found yosys in %s)" % opts.yosys)
 	
-	command = "./build/avr"
+	command = "./avr"
 	command = command + " " + f
 	command = command + " " + str(opts.top)
 	command = command + " " + path
@@ -266,7 +270,9 @@ def main():
 	if (opts.parse % 2 == 1):
 		parse_only = not DEFAULT_PARSE_ONLY
 	command = command + " " + str(parse_only)
-	
+
+	command = command + " " + str(opts.backend)
+
 	s = subprocess.call("exec " + command, shell=True)
 	if (s != 0):
 		raise Exception("avr ERROR: return code %d" % s)
diff --git a/avr_pr.py b/avr_pr.py
index 78032d2..f567b4f 100755
--- a/avr_pr.py
+++ b/avr_pr.py
@@ -16,7 +16,7 @@
 start_time = time.time()
 
 cmdSuffix = ""
-maxWorkers = 8
+maxWorkers = 16
 
 optSuffix = " "
 commands = []
@@ -30,14 +30,14 @@
 DEFAULT_NAME="test"
 DEFAULT_WORKERS="workers.txt"
 #DEFAULT_BIN="bin"
-DEFAULT_TIMEOUT=3600
-DEFAULT_MEMOUT=16000
+DEFAULT_TIMEOUT=3590
+DEFAULT_MEMOUT=118000
 DEFAULT_PRINT_SMT2=False
-DEFAULT_PRINT_WITNESS=True
+DEFAULT_PRINT_WITNESS=False
 
 maxTimeSec = DEFAULT_TIMEOUT
 maxMemMB = DEFAULT_MEMOUT
-maxInitW = 2
+maxInitW = 12
 resultW = 0
 out_path = DEFAULT_OUT + "/" + DEFAULT_NAME
 
diff --git a/deps/build_deps.sh b/deps/build_deps.sh
index c3de164..0fcd513 100755
--- a/deps/build_deps.sh
+++ b/deps/build_deps.sh
@@ -1,7 +1,7 @@
 #!/bin/bash -x
 set -e
 
-MATHSATVERSION="5.6.10"
+MATHSATVERSION="5.6.11"
 
 echo "Installing dependencies..."
 
diff --git a/src/Makefile b/src/Makefile
index abae79e..0d9a905 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,38 +1,45 @@
+#ENABLE_Y2 := 0
+#ENABLE_M5 := 0
+#ENABLE_BT := 0
+#ENABLE_Z3 := 0
+
 REA_LOC = reach
 DPA_LOC = dpa
 VWN_LOC = vwn
 
 all:
-	$(MAKE) da
-	$(MAKE) re
 	$(MAKE) vw
+	$(MAKE) da
+	ENABLE_Y2=1 $(MAKE) re
+	ENABLE_BT=1 $(MAKE) re
+#	ENABLE_M5=1 $(MAKE) re
 
 clean:
+	$(MAKE) vwc
 	$(MAKE) dac
 	$(MAKE) rec
-	$(MAKE) vwc
 	@echo Cleaning Complete
 
-re:
-	@cd $(REA_LOC); $(MAKE)
+vw:
+	@cd $(VWN_LOC) ; $(MAKE)
 	@echo
-	@echo %%% reach: Compilation Complete.
+	@echo %%% vwn: Compilation Complete.
 
 da:
 	@cd $(DPA_LOC); $(MAKE)
 	@echo
 	@echo %%% dpa: Compilation Complete.
 
-vw:
-	@cd $(VWN_LOC) ; $(MAKE)
+re:
+	@cd $(REA_LOC); $(MAKE)
 	@echo
-	@echo %%% vwn: Compilation Complete.
+	@echo %%% reach: Compilation Complete.
 
-rec:
-	@cd $(REA_LOC); $(MAKE) clean
+vwc:
+	@cd $(VWN_LOC) ; $(MAKE) clean
 
 dac:
 	@cd $(DPA_LOC); $(MAKE) clean
 
-vwc:
-	@cd $(VWN_LOC) ; $(MAKE) clean
+rec:
+	@cd $(REA_LOC); $(MAKE) clean
diff --git a/src/dpa/avr_word_netlist.h b/src/dpa/avr_word_netlist.h
index feb2098..e3c16da 100644
--- a/src/dpa/avr_word_netlist.h
+++ b/src/dpa/avr_word_netlist.h
@@ -623,6 +623,8 @@ class NumInst: public Inst {
 
 	// you can't call!
 	NumInst(unsigned long num, unsigned size, SORT sort) {
+		if (size == 1)
+			assert(num == 0 || num == 1);
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mpz_class(num);
@@ -632,6 +634,8 @@ class NumInst: public Inst {
 // 		m_mpz.set_str(snum, base);
 // 	}
 	NumInst(mpz_class mnum, unsigned size, SORT sort) {
+		if (size == 1)
+			assert(mnum.get_si() == 0 || mnum.get_si() == 1);
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mnum;
diff --git a/src/makefile.include b/src/makefile.include
index b64fc52..912c2d6 100644
--- a/src/makefile.include
+++ b/src/makefile.include
@@ -1,15 +1,5 @@
 STATIC_MODE := 0
 
-### enable/disable solver environments
-### by default, z3 environment is disabled
-### also choose a BACKEND_* flag in src/reach/reach_backend.h 
-### to change solver backends for different kinds of SMT queries
-###
-ENABLE_Y2 := 1
-ENABLE_M5 := 1
-ENABLE_BT := 1
-ENABLE_Z3 := 0
-
 ENABLE_VMT   := 1
 ENABLE_BTOR2 := 1
 
@@ -27,7 +17,6 @@ STATIC_GMP   = -lgmp
 STATIC_GMPXX = -lgmpxx
 
 ####	reach : reachability computation
-REACH_BIN = $(BIN_DIR)/reach
 REACH_OBJS = avr_word_netlist.o avr_util.o avr_config.o reach_sa.o reach_backend.o reach_z3.o reach_y2.o \
              reach_evaluate.o reach_coi.o reach_simulate.o reach_util.o reach_tsim.o reach_solve.o       \
              reach_cegar.o reach_core.o reach.o reach_cex.o reach_print.o reach_bmc.o reach_bool.o
@@ -53,7 +42,7 @@ ifeq ($(ENABLE_BTOR2), 1)
   VWN_OBJS += btor2_frontend.o btor2_parser.o
 endif
 
-GPP=g++ -std=c++11
+GPP=g++ -std=c++17
 
 ####	flags
 CFLAG_OPT = -g -O3
diff --git a/src/reach/Makefile b/src/reach/Makefile
index 1d12627..0433c90 100644
--- a/src/reach/Makefile
+++ b/src/reach/Makefile
@@ -10,20 +10,26 @@ else
   LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
 endif
 
+Y2_DIR = $(DEPS)/yices2
+Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a
+INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include
+LINKLIBS += $(Y2_LIB)
+CFLAGS += -D_Y2
 ifeq ($(ENABLE_Y2), 1)
-  Y2_DIR = $(DEPS)/yices2
-  Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a
-  INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include
-  LINKLIBS += $(Y2_LIB)
-  CFLAGS += -D_Y2
+  CFLAGS += -DBACKEND_Y2
+  REACH_SUFFIX = y2
 endif
 
-ifeq ($(ENABLE_Z3), 1)
-  Z3_DIR = $(DEPS)/z3
-  Z3_LIB = $(Z3_DIR)/build/lib/libz3.a
-  INCLUDE += -I$(Z3_DIR)/build/include
-  LINKLIBS += $(Z3_LIB)
-  CFLAGS += -D_Z3
+ifeq ($(ENABLE_BT), 1)
+  BT_DIR = $(DEPS)/boolector
+  BT_LIB = $(BT_DIR)/build/lib/libboolector.a
+  BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a
+  BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a
+  INCLUDE += -I$(BT_DIR)/src
+  LINKLIBS += $(BT_LIB)
+  CFLAGS += -D_BT
+  CFLAGS += -DBACKEND_BT
+  REACH_SUFFIX = bt
 endif
 
 ifeq ($(ENABLE_M5), 1)
@@ -32,16 +38,17 @@ ifeq ($(ENABLE_M5), 1)
   INCLUDE += -I$(MSAT_DIR)/include
   LINKLIBS += $(MSAT_LIB)
   CFLAGS += -D_M5
+  CFLAGS += -DBACKEND_M5
+  REACH_SUFFIX = m5
 endif
 
-ifeq ($(ENABLE_BT), 1)
-  BT_DIR = $(DEPS)/boolector
-  BT_LIB = $(BT_DIR)/build/lib/libboolector.a
-  BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a
-  BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a
-  INCLUDE += -I$(BT_DIR)/src
-  LINKLIBS += $(BT_LIB)
-  CFLAGS += -D_BT
+ifeq ($(ENABLE_Z3), 1)
+  Z3_DIR = $(DEPS)/z3
+  Z3_LIB = $(Z3_DIR)/build/lib/libz3.a
+  INCLUDE += -I$(Z3_DIR)/build/include
+  LINKLIBS += $(Z3_LIB)
+  CFLAGS += -D_Z3 -DBACKEND_Z3
+  REACH_SUFFIX = z3
 endif
 
 DEPDIR := .d
@@ -51,7 +58,10 @@ DEPFLAGS = -MT $@ -MMD -MP -MF $(DEPDIR)/$*.Td
 COMPILE.cc = $(CXX) $(DEPFLAGS) $(CFLAGS) $(INCLUDE)
 POSTCOMPILE = mv -f $(DEPDIR)/$*.Td $(DEPDIR)/$*.d
 
+REACH_BIN = $(BIN_DIR)/reach_$(REACH_SUFFIX)
+
 all:
+	rm -f *.o
 	$(MAKE) $(REACH_BIN)
 
 $(REACH_BIN):$(REACH_OBJS)
@@ -65,7 +75,7 @@ $(REACH_BIN):$(REACH_OBJS)
 
 clean:
 	rm -f *.o
-	rm -f $(REACH_BIN)
+	rm -f $(BIN_DIR)/reach*
 	rm -rf .d/
 
 $(DEPDIR)/%.d: ;
diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp
index f3573c9..04c9586 100644
--- a/src/reach/avr_word_netlist.cpp
+++ b/src/reach/avr_word_netlist.cpp
@@ -5427,16 +5427,16 @@ void OpInst::calc_size() {
 		assert((*cit)->get_type() == Num);
 		unsigned width = NumInst::as(*cit)->get_num();
 		cit++;
+		unsigned sz = NumInst::as(*cit)->get_num();
+		cit++;
 		assert((*cit)->get_type() == Num);
-		m_size = (*cit)->get_size();
+		m_size = sz;
 		m_sort.sz = m_size;
-		unsigned range = m_size;
-		assert(range > 0);
 
 		m_sort.type = arraytype;
 		m_sort.args.clear();
 		m_sort.args.push_back(SORT(width));
-		m_sort.args.push_back(SORT(range));
+		m_sort.args.push_back(SORT(m_size));
 		assert(m_size > 0);
 		assert(m_sort.sz > 0);
 	}
@@ -5643,7 +5643,7 @@ unsigned find_size(OpInst::OpType op, InstL& exps)
 		second++;
 		assert((*first)->get_type() == Num);
 		assert((*second)->get_type() == Num);
-		size = (*second)->get_size();
+		size = NumInst::as(*second)->get_num();
 		assert (size > 0);
 	}
 		break;
diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h
index 812e51c..ac0f07c 100644
--- a/src/reach/avr_word_netlist.h
+++ b/src/reach/avr_word_netlist.h
@@ -2155,6 +2155,8 @@ class NumInst: public Inst {
 
 	// you can't call!
 	NumInst(unsigned long num, unsigned size, bool fromSystem, SORT sort) {
+		if (size == 1)
+			assert(num == 0 || num == 1);
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mpz_class(num);
@@ -2188,6 +2190,8 @@ class NumInst: public Inst {
 // 		m_mpz.set_str(snum, base);
 // 	}
 	NumInst(mpz_class mnum, unsigned size, bool fromSystem, SORT sort) {
+		if (size == 1)
+			assert(mnum.get_si() == 0 || mnum.get_si() == 1);
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mnum;
diff --git a/src/reach/reach_backend.h b/src/reach/reach_backend.h
index b0dd9de..88a7ec7 100644
--- a/src/reach/reach_backend.h
+++ b/src/reach/reach_backend.h
@@ -26,7 +26,7 @@
 /// Configurations
 /// Note: Only one of the below flag should be enabled
 
-#define BACKEND_Y2		// Yices 2 for all queries
+// #define BACKEND_Y2		// Yices 2 for all queries
 // #define BACKEND_BT		// Yices 2 for abstract, Boolector for bv queries
 // #define BACKEND_M5		// Yices 2 for abstract, MathSAT 5 for bv queries
 
diff --git a/src/reach/reach_bt.cpp b/src/reach/reach_bt.cpp
index f54c2e6..df98c5c 100644
--- a/src/reach/reach_bt.cpp
+++ b/src/reach/reach_bt.cpp
@@ -1893,7 +1893,14 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 					int maxaddress = pow(2, width) - 1;
 					bool initialized = false;
 					for (int i = 0; i <= maxaddress; i++) {
-						string v = value.substr(i*size, size);
+						string v;
+						if (value.size() <= size) {
+							v = value;
+						} else if (value.size() > (i*size)) {
+							v = value.substr(i*size, size);
+						} else {
+							v = "0";
+						}
 						Inst* address = NumInst::create(maxaddress - i, width, SORT());
 						Inst* data = NumInst::create(v, size, 2, SORT());
 						bt_expr_ptr b = create_bt_number(NumInst::as(data));
@@ -2180,6 +2187,10 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 				case OpInst::AShiftR:
 				case OpInst::Sext:
 				case OpInst::Zext:
+				case OpInst::RotateL:
+				case OpInst::RotateR:
+				case OpInst::VRotateL:
+				case OpInst::VRotateR:
 				case OpInst::IntAdd:
 				case OpInst::IntSub:
 				case OpInst::IntMult:
@@ -2306,6 +2317,43 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 							res = boolector_uext(g_ctx, a2, amount);
 					}
 						break;
+					case OpInst::RotateL:
+					case OpInst::RotateR: {
+						assert(y_ch.size() == 2);
+						InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
+						ve_it2++;
+						NumInst* num = NumInst::as(*ve_it2);
+						cout << "Rotate: " << *e << endl;
+						if (num != 0)
+						{
+							int rotate_amount = num->get_mpz()->get_si() % e->get_size();
+							cout << "rotate_amount: " << rotate_amount << endl;
+							if (rotate_amount != 0) {
+								if (o == OpInst::RotateL)
+								{
+									res = boolector_roli(g_ctx, a, rotate_amount);
+								} else {
+									res = boolector_rori(g_ctx, a, rotate_amount);
+								}
+							} else {
+								res = a;
+							}
+						} else {
+							cout << "Expected second operand as number in " << *e << endl;
+							assert(0);
+						}
+					}
+						break;
+					case OpInst::VRotateL:{
+						assert(y_ch.size() == 2);
+						res = boolector_rol(g_ctx, a, b);
+					}
+						break;
+					case OpInst::VRotateR:{
+						assert(y_ch.size() == 2);
+						res = boolector_ror(g_ctx, a, b);
+					}
+						break;
 					case OpInst::IntAdd: {
 						bt_loge("unsupported");
 					}
@@ -2335,7 +2383,6 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 					}
 				}
 					break;
-
 				case OpInst::AddC:
 				case OpInst::AShiftL:
 					assert(0); // for now.
@@ -2364,15 +2411,6 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 						res = boolector_not(g_ctx, res);
 				}
 					break;
-				case OpInst::RotateR:
-				case OpInst::VRotateR:{
-					bt_loge("TODO");
-				}
-				  break;
-				case OpInst::RotateL:
-				case OpInst::VRotateL:{
-					bt_loge("TODO");
-				}
 				  break;
 				case OpInst::VShiftL:
 				case OpInst::VShiftR:
diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp
index ba29ba4..8ca0ae4 100644
--- a/src/reach/reach_cegar.cpp
+++ b/src/reach/reach_cegar.cpp
@@ -4517,7 +4517,9 @@ int Reach::ccext_block() {
 			s_check_result = y_solver.solver_main->s_check(AB_QUERY_TIMEOUT, false);
 			if (s_check_result == AVR_QUSAT) {
 				assumptions.clear();
-				cube = conjunct_cube.front();
+				if (!conjunct_cube.empty()) {
+					cube = conjunct_cube.front();
+				}
 				// possible in relational inputs (like vmt - gulwani_cegar1)
 				AVR_LOG(15, 0, "\t(warning: F[" << frameIdx << "] has become UNSAT)" << endl);
 
@@ -4966,10 +4968,9 @@ int Reach::ccext_block() {
 #ifdef AVR_ADD_INITS_ENABLE
 			Inst *ve_gcube_before = ve_gcube;
 			AVR_LOG(6, 1, "## call add_inits_to_gcube in ccext_block !" << endl);
-//			cout << "Cube: " << *cube << endl;
-//			cout << "Gcube: " << *ve_gcube << endl;
-//			cout << "Gcubes: " << gcubes << endl;
-//			cout << "Gcubes$: " << gcubes_next << endl;
+			// cout << "Cube: " << *cube << endl;
+			// cout << "Gcube: " << *ve_gcube << endl;
+			// cout << "Gcubes: " << gcubes << endl;
 
 			InstL conjunct_ve_gcube;
 			collect_cubes(ve_gcube, true);
diff --git a/src/reach/reach_coi.cpp b/src/reach/reach_coi.cpp
index 32eeb9e..bc1d72e 100644
--- a/src/reach/reach_coi.cpp
+++ b/src/reach/reach_coi.cpp
@@ -896,7 +896,13 @@ bool Reach::find_from_minset2(Solver* solver, Inst*e, InstS& relSig, InstS& relC
     	find_from_minset2(solver, child, relSig, relConst, relUFtype);
       e->coi.update(child->coi);
     }
-    else if (opT == OpInst::LogAnd || opT == OpInst::LogOr) {
+    else if (opT == OpInst::LogAnd
+    	|| opT == OpInst::LogNand
+    	|| opT == OpInst::LogOr
+		|| opT == OpInst::LogNor
+		|| opT == OpInst::LogXor
+		|| opT == OpInst::LogXNor
+		) {
       int eVal = get_bval(solver, e);
 //  	  AVR_LOG(9, 1, "[COI]: (sval) e: " << *e << "\t" << eVal << endl);
       if (eVal == INVALID_SVAL) {
@@ -939,7 +945,7 @@ bool Reach::find_from_minset2(Solver* solver, Inst*e, InstS& relSig, InstS& relC
     else {
       string ufType = op->get_euf_func_name();
       if (ufType == "0")
-        cout << "\t(error: unexpected uf type)\t" << *e << endl;
+        cout << "\t(error: unexpected uf type)\t" << *e << "\t" << op->get_op() << endl;
       assert (ufType != "0");
 
 //      if (_s_uf.find(e) != _s_uf.end()) {
diff --git a/src/reach/reach_core.cpp b/src/reach/reach_core.cpp
index bde30cc..94b99b7 100644
--- a/src/reach/reach_core.cpp
+++ b/src/reach/reach_core.cpp
@@ -273,7 +273,7 @@ void Reach::init_solv()
 #endif
 
 #ifdef BACKEND_M5
-	s += "+y2";
+	s += "+m5";
 #endif
 
 #ifdef BACKEND_BT
diff --git a/src/reach/reach_m5.cpp b/src/reach/reach_m5.cpp
index b9ee356..42089f0 100644
--- a/src/reach/reach_m5.cpp
+++ b/src/reach/reach_m5.cpp
@@ -2632,7 +2632,14 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) {
 
 					Inst* defval;
 					for (int i = 0; i <= maxaddress; i++) {
-						string v = value.substr(i*size, size);
+						string v;
+						if (value.size() <= size) {
+							v = value;
+						} else if (value.size() > (i*size)) {
+							v = value.substr(i*size, size);
+						} else {
+							v = "0";
+						}
 						Inst* data = NumInst::create(v, size, 2, SORT());
 						if (i == 0) {
 							defval = data;
diff --git a/src/reach/reach_util.cpp b/src/reach/reach_util.cpp
index 0328306..cdd72dd 100644
--- a/src/reach/reach_util.cpp
+++ b/src/reach/reach_util.cpp
@@ -401,17 +401,17 @@ Inst* Reach::replace_constant_with_value(Inst *top) {
   		Inst* num;
     	if (c->get_sort_type() == arraytype) {
     		if (c->get_sort_domain()->type == bvtype && c->get_sort_range()->type == bvtype) {
-					string value = top->get_ival()->get_str(2);
-					while (value.length() < c->get_size())
-						value = "0" + value;
+    				int width = c->get_sort_domain()->sz;
+    				int size = c->get_size();
+    				assert(size == c->get_sort_range()->sz);
 
-					int width = c->get_sort_domain()->sz;
-					int size = c->get_size();
-					assert(size == c->get_sort_range()->sz);
+    				string value = top->get_ival()->get_str(2);
+					while (value.length() < (c->get_size() * 2))
+						value = "0" + value;
 
 					Inst* wI = NumInst::create(width, 32, SORT());
 					Inst* sI = NumInst::create(size, 32, SORT());
-					Inst* dI = NumInst::create(value, size, 2, SORT());
+					Inst* dI = NumInst::create(value, value.length(), 2, SORT());
 					num = OpInst::create(OpInst::ArrayConst, wI, sI, dI);
     		}
     		else {
@@ -5746,52 +5746,37 @@ void Reach::check_correctness()
 	ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach);
 	res = int_solver->check_sat(ve_reach, 0, false);
 
-	if(res == false)
-	{
-		AVR_LOG(8, 0, "There is a wrong (UNSAT) reachability lemma!!!" << endl);
-
-		SOLVER_MUS tmpSolver(_abstract_mapper, AVR_EXTRA_IDX, true, regular);
-		tmpSolver.disable_fallback();
-		tmpSolver.assert_all_wire_constraints();
-		InstLL muses;
-		tmpSolver.get_muses_2(0, conjunct_reach, muses, num_scalls_sat_correctness, num_scalls_unsat_correctness, &tmpSolver);
-		cout << "mus: " << muses.front() << endl;
-		assert(0);
-	}
-	else
-	{
-		AVR_LOG(8, 0, "reachability-lemmas-check successful!" << endl);
-	}
 	delete static_cast<SOLVER_AB*>(int_solver);
 	/// END
 
-	/// Checking Refinements [SAT is correct]
-	if(_numRefinements > 0)
-	{
-		int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular);
-		int_solver->assert_all_wire_constraints();
-		conjunct_reach.clear();
-		for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3)
-			conjunct_reach.push_back(*it3);
-
-		ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach);
-		AVR_LOG(8, 6, "Checking Q:" << conjunct_reach);
-		bool res = int_solver->check_sat(ve_reach, 0, false);
-
-		if(res == false)
-		{
-			AVR_LOG(8, 0, "There is a wrong (UNSAT) datapath lemma!!!" << endl);
-			AVR_LOG(8, 0, "Possible errors include: incorrect assumptions" << endl);
-			int_solver->print_query(0, ERROR, "error");
-			assert(0);
-		}
-		else
-		{
-			AVR_LOG(8, 0, "DP-lemmas-check successful!" << endl);
-		}
-		delete static_cast<SOLVER_AB*>(int_solver);
-	}
-	/// END
+// 	/// Checking Refinements [SAT is correct]
+// 	if(_numRefinements > 0)
+// 	{
+// 		int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular);
+// 		int_solver->assert_all_wire_constraints();
+// 		conjunct_reach.clear();
+// 		for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3)
+// 			conjunct_reach.push_back(*it3);
+//
+// 		ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach);
+// 		AVR_LOG(8, 6, "Checking Q:" << conjunct_reach);
+// 		bool res = int_solver->check_sat(ve_reach, 0, false);
+//
+// 		if(res == false)
+// 		{
+// 			AVR_LOG(8, 0, "There is a wrong (UNSAT) datapath lemma!!!" << endl);
+// 			AVR_LOG(8, 0, "Possible errors include: incorrect assumptions" << endl);
+// 			int_solver->print_query(0, ERROR, "error");
+// 			AVR_LOG(8, 0, "Checking Q:" << conjunct_reach);
+// //			assert(0);
+// 		}
+// 		else
+// 		{
+// 			AVR_LOG(8, 0, "DP-lemmas-check successful!" << endl);
+// 		}
+// 		delete static_cast<SOLVER_AB*>(int_solver);
+// 	}
+// 	/// END
 
   /// (I & Refinements -> F[converged])
   int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular);
diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp
index c0e0ec3..6d15df5 100644
--- a/src/reach/reach_y2.cpp
+++ b/src/reach/reach_y2.cpp
@@ -5367,7 +5367,7 @@ bool y2_API::get_relation(Inst* lhs, Inst* rhs, bool expected)
 
 bool y2_API::get_assignment(Inst* e, int& val)
 {
-	assert(e->get_sort_type() == bvtype);
+	assert(e->get_sort_type() == bvtype || e->get_sort_type() == arraytype);
 	assert(m_model != NULL);
 
 	y2_expr decl = e->y2_node.solv_var(get_vIdx());
@@ -6004,6 +6004,9 @@ y2_expr_ptr y2_API::create_y2_number(NumInst* num) {
 			if (num->get_num() == 1)
 				return m_b1;
 			else {
+				if (num->get_num() != 0) {
+					cout << "num: " << *num << endl;
+				}
 				assert (num->get_num() == 0);
 				return m_b0;
 			}
@@ -6620,7 +6623,14 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 						value = "0" + value;
 					int maxaddress = pow(2, width) - 1;
 					for (int i = 0; i <= maxaddress; i++) {
-						string v = value.substr(i*size, size);
+						string v;
+						if (value.size() <= size) {
+							v = value;
+						} else if (value.size() > (i*size)) {
+							v = value.substr(i*size, size);
+						} else {
+							v = "0";
+						}
 						Inst* address = NumInst::create(maxaddress - i, width, SORT());
 						Inst* data = NumInst::create(v, size, 2, SORT());
 						y2_expr_ptr a = create_y2_number(NumInst::as(address));
@@ -7085,25 +7095,12 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 						assert(y_ch.size() == 2);
 						InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
 						ve_it2++;
-						NumInst* num = NumInst::as(*ve_it2);
-						if (num != 0)
-						{
-							if (o == OpInst::ShiftL)
-							{
-								res = yices_shift_left0(a, num->get_mpz()->get_si());
-							} else {
-								res = yices_shift_right0(a, num->get_mpz()->get_si());
-							}
-						}
+						if (o == OpInst::ShiftR)
+							res = yices_bvlshr(a, b);
+						else if (o == OpInst::ShiftL)
+							res = yices_bvshl(a, b);
 						else
-						{
-							if (o == OpInst::ShiftR)
-								res = yices_bvlshr(a, b);
-							else if (o == OpInst::ShiftL)
-								res = yices_bvshl(a, b);
-							else
-								assert(0);
-						}
+							assert(0);
 						assert(res != -1);
 					}
 						break;
@@ -7111,16 +7108,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 						assert(y_ch.size() == 2);
 						InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
 						ve_it2++;
-						NumInst* num = NumInst::as(*ve_it2);
-						if (num != 0)
-						{
-							res = yices_ashift_right(a, num->get_mpz()->get_si());
-							assert(res != -1);
-						}
-						else
-						{
-							res = yices_bvashr(a, b);
-						}
+						res = yices_bvashr(a, b);
 						assert(res != -1);
 					}
 						break;
@@ -7240,6 +7228,10 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 						cout << "Expected second operand as number in " << *e << endl;
 						assert(0);
 					}
+					if (res == -1) {
+						cout << "e: " << *e << endl;
+						cout << yices_error_string() << endl;
+					}
 					assert(res != -1);
 				}
 					break;
diff --git a/src/reach/reach_z3.cpp b/src/reach/reach_z3.cpp
index 609756a..50e5293 100644
--- a/src/reach/reach_z3.cpp
+++ b/src/reach/reach_z3.cpp
@@ -5372,22 +5372,7 @@ void z3_API::inst2yices(Inst*e, bool bvAllConstraints)
 						assert(y_ch.size() == 2);
 						InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
 						ve_it2++;
-						NumInst* num = NumInst::as(*ve_it2);
-						if (num != 0)
 						{
-							if (o == OpInst::ShiftL)
-							{
-								z3_expr_ptr sExpr = new z3_expr(*g_ctx);
-								*sExpr = shl(term(a), num->get_mpz()->get_si());
-								res = sExpr;
-							}
-							else {
-								z3_expr_ptr sExpr = new z3_expr(*g_ctx);
-								*sExpr = lshr(term(a), num->get_mpz()->get_si());
-								res = sExpr;
-							}
-						}
-						else {
 							if (o == OpInst::ShiftR)
 							{
 								z3_expr_ptr sExpr = new z3_expr(*g_ctx);
diff --git a/src/vwn/avr_word_netlist.h b/src/vwn/avr_word_netlist.h
index 1cd05d2..3026759 100644
--- a/src/vwn/avr_word_netlist.h
+++ b/src/vwn/avr_word_netlist.h
@@ -660,6 +660,8 @@ class NumInst: public Inst {
 
 	// you can't call!
 	NumInst(unsigned long num, unsigned size, SORT sort) {
+		if (size == 1)
+			assert(num == 0 || num == 1);
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mpz_class(num);
@@ -673,6 +675,9 @@ class NumInst: public Inst {
 // 		m_mpz.set_str(snum, base);
 // 	}
 	NumInst(mpz_class mnum, unsigned size, SORT sort) {
+		if (size == 1) {
+			assert(mnum.get_si() == 0 || mnum.get_si() == 1);
+		}
 		m_sort = sort;
 		m_size = size;
 		m_mpz = mnum;
diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp
index e13c962..4ba3531 100644
--- a/src/vwn/btor2_frontend.cpp
+++ b/src/vwn/btor2_frontend.cpp
@@ -306,7 +306,7 @@ Inst* Btor2Frontend::get_init(Btor2Line& t, int sz, SORT sort, InstL& args) {
 				InstL args;
 				args.push_back(NumInst::create(width, 32));
 				args.push_back(NumInst::create(sz, 32));
-				args.push_back(NumInst::create(*value, sz));
+				args.push_back(NumInst::create(*value, init_val->get_size()));
 				rhs = OpInst::create(OpInst::ArrayConst, args);
 				done = true;
 			}
@@ -508,6 +508,9 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
 	} break;
 	case BTOR2_TAG_constd: {
 		string snum(t.constant);
+		if (sz == 1 && snum != "1") {
+			snum = "0";
+		}
 		node = NumInst::create(snum, sz, 10, sort);
 //		{
 //			string numstr = NumInst::as(node)->get_mpz()->get_str(10);
diff --git a/src/vwn/ilang_frontend.cpp b/src/vwn/ilang_frontend.cpp
index 2958418..5170e61 100644
--- a/src/vwn/ilang_frontend.cpp
+++ b/src/vwn/ilang_frontend.cpp
@@ -1586,7 +1586,7 @@ void IlangFrontend::process_memory(Cell& c) {
 
 		args.push_back(NumInst::create(width, 32));
 		args.push_back(NumInst::create(size, 32));
-		args.push_back(NumInst::create(*value, size));
+		args.push_back(NumInst::create(*value, init_val->get_size()));
 		Inst* rhs = OpInst::create(OpInst::ArrayConst, args);
 		initials.push_back(OpInst::create(OpInst::Eq, pre, rhs));
 		map_init[pre] = rhs;
diff --git a/workers.txt b/workers.txt
index 3e2bfa6..8410bcd 100755
--- a/workers.txt
+++ b/workers.txt
@@ -1,14 +1,16 @@
-python3 avr.py --bin build/bin
-python3 avr.py --bin build/bin --abstract sa
-python3 avr.py --bin build/bin --abstract sa --kind
-python3 avr.py --bin build/bin --abstract sa --bmc
-python3 avr.py --bin build/bin --split
-# python3 avr.py --bin build/bin_bt_cad
-# python3 avr.py --bin build/bin_bt_cad --abstract sa
-python3 avr.py --bin build/bin --abstract sa8
-python3 avr.py --bin build/bin --abstract sa16
-python3 avr.py --bin build/bin --abstract sa32
-python3 avr.py --bin build/bin --level 0
-python3 avr.py --bin build/bin --level 5
-python3 avr.py --bin build/bin --interpol 1
-python3 avr.py --bin build/bin --forward 1
+python3 avr.py --split
+python3 avr.py
+python3 avr.py --abstract sa
+python3 avr.py --kind --backend bt
+python3 avr.py --abstract sa4 --split --interpol 1 --forward 1
+python3 avr.py --bmc --abstract sa --split --backend bt
+python3 avr.py --kind --split
+python3 avr.py --abstract sa8 --split --interpol 1
+python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
+python3 avr.py --split --backend bt
+python3 avr.py --kind --split
+python3 avr.py --split --level 0
+python3 avr.py --abstract sa --interpol 1 --forward 1 --backend bt
+python3 avr.py --bmc --split
+python3 avr.py --abstract sa32 --granularity 3 --level 0 --backend bt
+python3 avr.py --abstract sa16 --split --forward 1 --backend bt
\ No newline at end of file