diff --git a/src/main.rs b/src/main.rs
index 0abe900..dfd2cfd 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,7 +16,7 @@ use rhoevm::modules::expr::is_function_sig_check_prop;
 use rhoevm::modules::format::{hex_byte_string, strip_0x};
 use rhoevm::modules::smt::parse_z3_output;
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, VM, W256};
+use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 #[derive(Debug)]
 struct Args {
@@ -118,7 +118,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };
diff --git a/src/modules/cli.rs b/src/modules/cli.rs
index fdaac02..3c004ba 100644
--- a/src/modules/cli.rs
+++ b/src/modules/cli.rs
@@ -11,7 +11,7 @@ use crate::modules::format::{hex_byte_string, strip_0x};
 use crate::modules::symexec::mk_calldata;
 use crate::modules::transactions::init_tx;
 use crate::modules::types::{
-  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, VM, W256,
+  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, EXPR_MEMPTY, VM, W256,
 };
 
 type URL = String;
@@ -110,7 +110,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
           Some(code) => {
             let bs = hex_byte_string("bytes", &strip_0x(code));
             let mc = if cmd.create {
-              ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+              ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
             } else {
               ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
             };
@@ -127,7 +127,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };
diff --git a/src/modules/evm.rs b/src/modules/evm.rs
index d719195..5f299e4 100644
--- a/src/modules/evm.rs
+++ b/src/modules/evm.rs
@@ -27,7 +27,7 @@ use crate::modules::types::{
   word256_bytes, Addr, BaseState, Block, BranchDir, BranchReachability, ByteString, Cache, CodeLocation, Contract,
   ContractCode, Env, EvmError, Expr, ExprSet, ForkState, Frame, FrameContext, FrameState, Gas, Memory, MutableMemory,
   PartialExec, Prop, RuntimeCodeStruct, RuntimeConfig, SubState, Trace, TraceData, TxState, VMOpts, VMResult,
-  W256W256Map, VM, W256, W64,
+  W256W256Map, EXPR_MEMPTY, VM, W256, W64,
 };
 
 fn initial_gas() -> u64 {
@@ -52,11 +52,11 @@ pub fn blank_state() -> FrameState {
     stack: Vec::new(),
     memory: Memory::ConcreteMemory(Vec::new()),
     memory_size: 0,
-    calldata: Box::new(Expr::Mempty),
+    calldata: Box::new(EXPR_MEMPTY),
     callvalue: Box::new(Expr::Lit(W256(0, 0))),
     caller: Box::new(Expr::LitAddr(W256(0, 0))),
     gas: Gas::Concerete(initial_gas()),
-    returndata: Box::new(Expr::Mempty),
+    returndata: Box::new(EXPR_MEMPTY),
     static_flag: false,
     prev_model: None,
   }
@@ -65,7 +65,7 @@ pub fn blank_state() -> FrameState {
 /// Retrieves the bytecode of a contract as an expression.
 ///
 /// This function examines the contract's code and returns the corresponding expression:
-/// - If the contract code is initialization code, an empty expression (`Expr::Mempty`) is returned.
+/// - If the contract code is initialization code, an empty expression (`EXPR_MEMPTY`) is returned.
 /// - If the contract code is runtime code, a concrete buffer containing the code is returned.
 ///
 /// # Arguments
@@ -77,7 +77,7 @@ pub fn blank_state() -> FrameState {
 /// An `Option<Expr>` containing the bytecode expression, or `None` if the contract code is unsupported.
 pub fn bytecode(contract: &Contract) -> Option<Expr> {
   match &contract.code {
-    ContractCode::InitCode(_, _) => Some(Expr::Mempty),
+    ContractCode::InitCode(_, _) => Some(EXPR_MEMPTY),
     ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(buf)) => Some(Expr::ConcreteBuf(buf.to_vec())),
     _ => None,
   }
@@ -171,7 +171,7 @@ pub fn make_vm(opts: VMOpts) -> VM {
       callvalue: Box::new(opts.value),
       caller: Box::new(opts.caller),
       gas: opts.gas,
-      returndata: Box::new(Expr::Mempty),
+      returndata: Box::new(EXPR_MEMPTY),
       static_flag: false,
       prev_model: None,
     },
@@ -422,7 +422,7 @@ impl VM {
       }
       true
     } else if self.state.pc >= opslen(&self.state.code) {
-      finish_frame(self, FrameResult::FrameReturned(Expr::Mempty));
+      finish_frame(self, FrameResult::FrameReturned(EXPR_MEMPTY));
       false
     } else {
       let op = match &self.state.code {
@@ -538,7 +538,7 @@ impl VM {
           true
         }
         Op::Stop => {
-          finish_frame(self, FrameResult::FrameReturned(Expr::Mempty));
+          finish_frame(self, FrameResult::FrameReturned(EXPR_MEMPTY));
           false
         }
         Op::Add => stack_op2(self, fees.g_verylow, "add"),
@@ -603,7 +603,7 @@ impl VM {
         }
         Op::Balance => {
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut a: Expr = Expr::Mempty;
+            let mut a: Expr = EXPR_MEMPTY;
             force_addr(self, x, "BALANCE", |a_| a = a_);
             access_and_burn(&a, || {
               let mut c = empty_contract();
@@ -759,7 +759,7 @@ impl VM {
           - size: byte size of the code.
           */
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut a: Expr = Expr::Mempty;
+            let mut a: Expr = EXPR_MEMPTY;
             force_addr(self, x, "EXTCODESIZE", |a_| a = a_);
             access_and_burn(&a, || {
               let mut c = empty_contract();
@@ -1013,7 +1013,7 @@ impl VM {
             let x = self.state.stack.pop().unwrap();
             let new = self.state.stack.pop().unwrap();
             // Access current storage
-            let mut current: Expr = Expr::Mempty;
+            let mut current: Expr = EXPR_MEMPTY;
             access_storage(self, *self_contract.clone(), *x.clone(), |current_| current = current_);
             let original = match conc_keccak_simp_expr(Box::new(Expr::SLoad(
               x.clone(),
@@ -1251,12 +1251,12 @@ impl VM {
             if gt0 == BranchReachability::ONLYTHEN || gt0 == BranchReachability::BOTH {
               not_static(self, || {});
 
-              let mut x_to_a = Expr::Mempty;
+              let mut x_to_a = EXPR_MEMPTY;
               force_addr(self, x_to, "unable to determine a call target", |x_to_a_| x_to_a = x_to_a_);
               match Some(x_gas) {
                 None => vm_error("IllegalOverflow"),
                 _ => {
-                  let mut callee: Expr = Expr::Mempty;
+                  let mut callee: Expr = EXPR_MEMPTY;
                   general_call(
                     self,
                     op,
@@ -1275,7 +1275,7 @@ impl VM {
                   );
                   let from_ = self.config.override_caller.clone();
                   let scaller =
-                    if let Some(_) = from_ { Box::new(from_.clone().unwrap()) } else { Box::new(Expr::Mempty) };
+                    if let Some(_) = from_ { Box::new(from_.clone().unwrap()) } else { Box::new(EXPR_MEMPTY) };
                   self.state.callvalue = x_value.clone();
                   self.state.caller = scaller.clone();
                   self.state.contract = Box::new(callee.clone());
@@ -1478,7 +1478,7 @@ impl VM {
                   // gasTryFrom(x_gas)
                   None => vm_error("IllegalOverflow"),
                   _ => {
-                    let mut callee = Expr::Mempty;
+                    let mut callee = EXPR_MEMPTY;
                     general_call(
                       self,
                       op,
@@ -1520,7 +1520,7 @@ impl VM {
         Op::Selfdestruct => {
           not_static(self, || {});
           if let [.., x_to] = &self.state.stack.clone()[..] {
-            let mut x_to_a = Expr::Mempty;
+            let mut x_to_a = EXPR_MEMPTY;
             force_addr(self, x_to, "SELFDESTRUCT", |x_to_a_| x_to_a = x_to_a_);
             if let Expr::WAddr(_) = x_to_a {
               let acc = access_account_for_gas(self, x_to_a.clone());
@@ -1552,7 +1552,7 @@ impl VM {
                 // });
               } else {
                 let mut else_vm = else_vm_.unwrap();
-                finish_frame(&mut else_vm, FrameResult::FrameReturned(Expr::Mempty));
+                finish_frame(&mut else_vm, FrameResult::FrameReturned(EXPR_MEMPTY));
               }
             } else {
               let pc = 0; // use(state.pc)
@@ -1579,7 +1579,7 @@ impl VM {
         }
         Op::Extcodecopy => {
           if let [xs @ .., code_size, code_offset, mem_offset, ext_account] = &self.state.stack.clone()[..] {
-            let mut ext_account_a = Expr::Mempty;
+            let mut ext_account_a = EXPR_MEMPTY;
             force_addr(self, ext_account, "EXTCODECOPY", |ext_account_a_| ext_account_a = ext_account_a_);
             burn_extcodecopy(self, ext_account_a.clone(), *code_size.clone(), self.block.schedule.clone(), || {});
             access_memory_range(self, &mem_offset, &code_size, || {});
@@ -1660,7 +1660,7 @@ impl VM {
         }
         Op::Extcodehash => {
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut addr = Expr::Mempty;
+            let mut addr = EXPR_MEMPTY;
             force_addr(self, x, "EXTCODEHASH", |addr_| addr = addr_);
             access_and_burn(&addr, || {
               next(self, op);
@@ -1856,7 +1856,7 @@ fn execute_precompile(
       } else {
         vm.state.stack = xs;
         vm.state.stack.push(Box::new(Expr::Lit(W256(1, 0))));
-        vm.state.returndata = Box::new(Expr::Mempty);
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
         next(vm, 0x00)
       }
     }
@@ -1947,7 +1947,6 @@ fn fetch_account<F: FnOnce(&Contract)>(vm: &mut VM, addr: &Expr, f: F) {
         }
       },
       Expr::GVar(_) => panic!("unexpected GVar"),
-      Expr::Mempty => {}
       _ => panic!("unexpected expr in `fetch_account`: addr={}", addr),
     },
   }
@@ -2071,7 +2070,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameErrored(_) => {
               vm.env.contracts = callreversion.clone();
               vm.tx.substate = substate.clone();
-              vm.state.returndata = Box::new(Expr::Mempty);
+              vm.state.returndata = Box::new(EXPR_MEMPTY);
               push(vm, W256(0, 0));
             }
           }
@@ -2096,7 +2095,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameReturned(output) => {
               let mut on_contract_code = |contract_code| {
                 replace_code(vm, createe.clone(), contract_code);
-                vm.state.returndata = Box::new(Expr::Mempty);
+                vm.state.returndata = Box::new(EXPR_MEMPTY);
                 // reclaimRemainingGasAllowance oldVm
                 push_addr(vm, *createe.clone());
               };
@@ -2129,7 +2128,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameErrored(_) => {
               vm.env.contracts = reversion_prime;
               vm.tx.substate = substate.clone();
-              vm.state.returndata = Box::new(Expr::Mempty);
+              vm.state.returndata = Box::new(EXPR_MEMPTY);
               push(vm, W256(0, 0));
             }
           }
@@ -2349,7 +2348,7 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
           &(Expr::Lit(W256(0, 0))),
           &(simplify(Box::new(size_.clone()))),
           &(buf),
-          &(Expr::Mempty),
+          &(EXPR_MEMPTY),
         )
       }
     },
@@ -2358,7 +2357,7 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
       &(Expr::Lit(W256(0, 0))),
       &(simplify(Box::new(size_.clone()))),
       &(simplify(Box::new(mem.clone()))),
-      &(Expr::Mempty),
+      &(EXPR_MEMPTY),
     ),
   }
 }
@@ -2394,7 +2393,7 @@ fn stack_op2(vm: &mut VM, gas: u64, op: &str) -> bool {
       "shl" => Box::new(Expr::SHL(a.clone(), b.clone())),
       "shr" => Box::new(Expr::SHR(a.clone(), b.clone())),
       "sar" => Box::new(Expr::SAR(a.clone(), b.clone())),
-      _ => Box::new(Expr::Mempty),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2412,7 +2411,7 @@ fn stack_op3(vm: &mut VM, gas: u64, op: &str) -> bool {
     let res = match op {
       "addmod" => Box::new(Expr::AddMod(a.clone(), b.clone(), c.clone())),
       "mulmod" => Box::new(Expr::MulMod(a.clone(), b.clone(), c.clone())),
-      _ => Box::new(Expr::Mempty),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2430,8 +2429,8 @@ fn stack_op1(vm: &mut VM, gas: u64, op: &str) -> bool {
     let res = match op {
       "iszero" => Box::new(Expr::IsZero(a.clone())),
       "not" => Box::new(Expr::Not(a.clone())),
-      "calldataload" => read_word(&a, &vm.state.calldata.clone()), // Box::new(Expr::Mempty),
-      _ => Box::new(Expr::Mempty),
+      "calldataload" => read_word(&a, &vm.state.calldata.clone()), // Box::new(EXPR_MEMPTY),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2721,8 +2720,8 @@ fn general_call(
       |x_gas_| x_gas = x_gas_,
       max_num_iterations,
     );
-    let mut target_code = ContractCode::UnKnownCode(Box::new(Expr::Mempty));
-    let mut taregt_codehash = Expr::Mempty;
+    let mut target_code = ContractCode::UnKnownCode(Box::new(EXPR_MEMPTY));
+    let mut taregt_codehash = EXPR_MEMPTY;
     fetch_account(vm, &x_to.clone(), |target| {
       target_code = target.code.clone();
       taregt_codehash = target.codehash.clone();
@@ -2764,7 +2763,7 @@ fn general_call(
         // update the state
         let new_memory = Memory::ConcreteMemory(vec![]);
         let cleared_init_code = match target_code {
-          ContractCode::InitCode(_, _) => ContractCode::InitCode(Box::new(vec![]), Box::new(Expr::Mempty)),
+          ContractCode::InitCode(_, _) => ContractCode::InitCode(Box::new(vec![]), Box::new(EXPR_MEMPTY)),
           a => a.clone(),
         };
         vm.state = FrameState {
@@ -2776,7 +2775,7 @@ fn general_call(
           stack: vec![],
           memory: new_memory,
           memory_size: 0,
-          returndata: Box::new(Expr::Mempty),
+          returndata: Box::new(EXPR_MEMPTY),
           calldata: Box::new(calldata.clone()),
           contract: vm.state.contract.clone(),
           callvalue: vm.state.callvalue.clone(),
@@ -2811,18 +2810,18 @@ fn create(
   if x_size_val > vm.block.max_code_size.clone() * W256(2, 0) {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     // vm_error(EvmError::MaxInitCodeSizeExceeded(vm0.block.max_code_size * 2, x_size));
   } else if this.nonce == Some(u64::max_value()) {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::NonceOverflow)));
     next(vm, op);
   } else if vm.frames.len() >= 1024 {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
     next(vm, op);
   } else if collision(vm.env.contracts.get(&new_addr).cloned()) {
@@ -2830,7 +2829,7 @@ fn create(
     burn(vm, x_gas_val, || {});
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     let n = vm.env.contracts.entry(self_addr.clone()).or_insert(empty_contract()).nonce;
     let new_nonce = if let Some(n_) = n { Some(n_ + 1) } else { None };
     vm.env.contracts.entry(self_addr).or_insert(empty_contract()).nonce = new_nonce;
@@ -2847,7 +2846,7 @@ fn create(
       // not enough balance
       vm.state.stack = xs.clone();
       vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-      vm.state.returndata = Box::new(Expr::Mempty);
+      vm.state.returndata = Box::new(EXPR_MEMPTY);
       vm.traces.push(with_trace_location(
         vm,
         TraceData::ErrorTrace(EvmError::BalanceTooLow(Box::new(x_value.clone()), Box::new(this.balance.clone()))),
@@ -3172,6 +3171,13 @@ fn account_empty(c: &Contract) -> bool {
 ///   and the second element is an optional string containing the model from the SMT solver if the constraints are satisfiable.
 pub async fn solve_constraints(pc: usize, pathconds: Vec<Box<Prop>>) -> (bool, Option<String>) {
   let result = task::spawn_blocking(move || {
+    /*
+    for p in &pathconds {
+      warn!("{} ", format_prop(p));
+    }
+    warn!("-------");
+    */
+
     let config = Config::default();
     let smt2 = assert_props(&config, pathconds.to_vec());
     if smt2.is_none() {
@@ -3393,7 +3399,7 @@ fn cheat_code() -> Expr {
 /// * `Option<ContractCode>` - The parsed initialization code, or `None` if parsing fails.
 fn parse_init_code(buf: &Expr) -> Option<ContractCode> {
   match buf {
-    Expr::ConcreteBuf(b) => Some(ContractCode::InitCode(Box::new(b.to_vec()), Box::new(Expr::Mempty))),
+    Expr::ConcreteBuf(b) => Some(ContractCode::InitCode(Box::new(b.to_vec()), Box::new(EXPR_MEMPTY))),
     _ => {
       let conc = concrete_prefix(buf);
       if conc.is_empty() {
@@ -3452,7 +3458,7 @@ fn call_checks<F>(
       if vm.frames.len() >= 1024 {
         vm.state.stack = xs.to_vec();
         vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-        vm.state.returndata = Box::new(Expr::Mempty);
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
         vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
         next(vm, op);
       } else {
@@ -3471,7 +3477,7 @@ fn call_checks<F>(
       if is_greater == BranchReachability::ONLYELSE || is_greater == BranchReachability::BOTH {
         vm.state.stack = xs.to_vec();
         vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-        vm.state.returndata = Box::new(Expr::Mempty);
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
         vm.traces.push(with_trace_location(
           vm,
           TraceData::ErrorTrace(EvmError::BalanceTooLow(Box::new(x_value), Box::new(this.balance.clone()))),
@@ -3483,7 +3489,7 @@ fn call_checks<F>(
         if else_vm.frames.len() >= 1024 {
           else_vm.state.stack = xs.to_vec();
           else_vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-          else_vm.state.returndata = Box::new(Expr::Mempty);
+          else_vm.state.returndata = Box::new(EXPR_MEMPTY);
           else_vm.traces.push(with_trace_location(&else_vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
           next(&mut else_vm, op);
         } else {
diff --git a/src/modules/expr.rs b/src/modules/expr.rs
index 9b61898..354a687 100644
--- a/src/modules/expr.rs
+++ b/src/modules/expr.rs
@@ -7,7 +7,8 @@ use crate::modules::cse::BufEnv;
 use crate::modules::rlp::{rlp_addr_full, rlp_list, rlp_word_256};
 use crate::modules::traversals::{fold_expr, map_expr, map_prop, map_prop_prime};
 use crate::modules::types::{
-  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, W256, W64,
+  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, EXPR_MEMPTY,
+  W256, W64,
 };
 
 use super::types::{ByteString, Word8};
@@ -871,7 +872,11 @@ pub fn copy_slice(src_offset: &Expr, dst_offset: &Expr, size: &Expr, src: &Expr,
         let sl: Vec<Expr> = ((src_offset.0)..(src_offset.0) + (size.0))
           .map(|i| read_byte(Box::new(Expr::Lit(W256(i as u128, 0))), Box::new(src.clone())))
           .collect();
-        let tl = &dst_buf[dst_offset.0 as usize + size.0 as usize..];
+        let tl = if (dst_offset.0 as usize + size.0 as usize) < dst_buf.len() {
+          &dst_buf[dst_offset.0 as usize + size.0 as usize..]
+        } else {
+          &vec![]
+        };
 
         if sl.iter().all(|arg0: &Expr| is_lit_byte(Box::new(arg0.clone()))) {
           let packed_sl: Vec<u8> = sl.into_iter().filter_map(maybe_lit_byte).collect();
@@ -1012,15 +1017,11 @@ fn conc_keccak_one_pass(expr: Box<Expr>) -> Expr {
 
 // Main simplify function
 pub fn simplify(expr: Box<Expr>) -> Expr {
-  if *expr != Expr::Mempty {
-    let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
-    if simplified == *expr {
-      simplified
-    } else {
-      simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
-    }
+  let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
+  if simplified == *expr {
+    simplified
   } else {
-    Expr::Mempty
+    simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
   }
 }
 
@@ -1872,7 +1873,7 @@ pub fn drop(n: W256, buf: &Expr) -> Expr {
 }
 
 pub fn slice(offset: Box<Expr>, size: Box<Expr>, src: Box<Expr>) -> Expr {
-  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(Expr::Mempty))
+  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(EXPR_MEMPTY))
 }
 
 pub fn buf_length(buf: &Expr) -> Expr {
@@ -1905,7 +1906,6 @@ pub fn buf_length_env(env: &HashMap<usize, Expr>, use_env: bool, buf: Expr) -> E
           emax(Box::new(l), Box::new(Expr::BufLength(Box::new(Expr::GVar(GVar::BufVar(a))))))
         }
       }
-      Expr::Mempty => l,
       _ => panic!("unsupported expression: {}", buf),
     }
   }
diff --git a/src/modules/smt.rs b/src/modules/smt.rs
index 5efade0..0944a55 100644
--- a/src/modules/smt.rs
+++ b/src/modules/smt.rs
@@ -1,3 +1,4 @@
+use log::info;
 use regex::Regex;
 use std::collections::{HashMap, HashSet};
 use std::{fmt, vec};
@@ -12,7 +13,7 @@ use crate::modules::expr::{
 use crate::modules::format::format_prop;
 use crate::modules::keccak::{keccak_assumptions, keccak_compute};
 use crate::modules::traversals::{fold_prop, TraversableTerm};
-use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, W256};
+use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, EXPR_MEMPTY, W256};
 
 // Type aliases for convenience
 type Text = String;
@@ -1103,7 +1104,7 @@ fn expr_to_smt(expr: Expr) -> String {
     },
     Expr::ReadByte(idx, src) => op2("select", *src, *idx),
     Expr::ConcreteBuf(bs) if bs.len() == 0 => "((as const Buf) #b00000000)".to_string(),
-    Expr::ConcreteBuf(bs) => write_bytes(&bs, Expr::Mempty),
+    Expr::ConcreteBuf(bs) => write_bytes(&bs, EXPR_MEMPTY),
     Expr::AbstractBuf(s) => s,
     Expr::ReadWord(idx, prev) => op2("readWord", *idx, *prev),
 
@@ -1243,7 +1244,7 @@ fn expand_exp(base: Expr, expnt: W256) -> Builder {
 
 // Concatenates a list of bytes into a larger bitvector
 fn write_bytes(bytes: &[u8], buf: Expr) -> Builder {
-  let skip_zeros = buf == Expr::Mempty;
+  let skip_zeros = buf == EXPR_MEMPTY;
   let mut idx = 0;
   let mut inner = expr_to_smt(buf);
   for &byte in bytes {
diff --git a/src/modules/traversals.rs b/src/modules/traversals.rs
index 1cc0d1b..216aba4 100644
--- a/src/modules/traversals.rs
+++ b/src/modules/traversals.rs
@@ -355,11 +355,7 @@ pub fn fold_expr<B>(f: &mut dyn FnMut(&Expr) -> B, acc: B, expr: &Expr) -> B
 where
   B: Add<B, Output = B> + Default + Clone,
 {
-  if *expr == Expr::Mempty {
-    acc.clone()
-  } else {
-    acc.clone() + go_expr(f, acc.clone(), expr.clone())
-  }
+  acc.clone() + go_expr(f, acc.clone(), expr.clone())
 }
 
 /// A trait for types that can map a function over their `Expr` components.
@@ -777,7 +773,6 @@ impl ExprMappable for Expr {
         let a = a.map_expr_m(f);
         f(&Expr::BufLength(Box::new(a)))
       }
-      Expr::Mempty => Expr::Mempty,
       _ => panic!("unuexpected expr {}", self),
     }
   }
@@ -798,11 +793,7 @@ pub fn map_expr<F>(mut f: F, expr: Expr) -> Expr
 where
   F: FnMut(&Expr) -> Expr,
 {
-  if expr == Expr::Mempty {
-    expr
-  } else {
-    expr.map_expr_m(&mut f)
-  }
+  expr.map_expr_m(&mut f)
 }
 
 /// Recursively applies a given function `f` to each `Expr` within a `Prop`.
diff --git a/src/modules/types.rs b/src/modules/types.rs
index 617f8fa..e6a0532 100644
--- a/src/modules/types.rs
+++ b/src/modules/types.rs
@@ -402,7 +402,6 @@ impl fmt::Display for GVar {
 
 #[derive(Debug, Clone)]
 pub enum Expr {
-  Mempty,
   // Identifiers
   Lit(W256),
   Var(String),
@@ -515,7 +514,6 @@ pub enum Expr {
 impl fmt::Display for Expr {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
-      Expr::Mempty => write!(f, "Mempty"),
       Expr::Lit(val) => write!(f, "Lit(0x{})", val.to_hex()),
       Expr::Var(name) => write!(f, "Var({})", name),
       Expr::GVar(gvar) => write!(f, "GVar({})", gvar),
@@ -601,6 +599,8 @@ impl fmt::Display for Expr {
   }
 }
 
+pub const EXPR_MEMPTY: Expr = Expr::ConcreteBuf(vec![]);
+
 impl Eq for Expr {}
 
 impl PartialEq for Expr {
@@ -608,7 +608,6 @@ impl PartialEq for Expr {
     use Expr::*;
 
     match (self, other) {
-      (Mempty, Mempty) => true,
       (Lit(val1), Lit(val2)) => val1 == val2,
       (Var(name1), Var(name2)) => name1 == name2,
       (GVar(gvar1), GVar(gvar2)) => gvar1 == gvar2,
@@ -710,9 +709,6 @@ impl Hash for Expr {
     use Expr::*;
 
     match self {
-      Mempty => {
-        "Mempty".hash(state);
-      }
       Lit(val) => {
         "Lit".hash(state);
         val.hash(state);
@@ -1167,7 +1163,7 @@ pub fn update_balance(c: Contract, new_balance: Expr) -> Contract {
 impl Contract {
   pub fn bytecode(&self) -> Option<Expr> {
     match &self.code {
-      ContractCode::InitCode(_, _) => Some(Expr::Mempty), // Equivalent to Just mempty
+      ContractCode::InitCode(_, _) => Some(EXPR_MEMPTY), // Equivalent to Just mempty
       ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(bs)) => Some(Expr::ConcreteBuf(*bs.clone())),
       ContractCode::RuntimeCode(RuntimeCodeStruct::SymbolicRuntimeCode(ops)) => Some(from_list(ops.to_vec())),
       ContractCode::UnKnownCode(_) => None,
@@ -1587,7 +1583,7 @@ where
 // Implement the Default trait for AddableVec
 impl Default for Expr {
   fn default() -> Expr {
-    Expr::Mempty // Return an empty vector
+    EXPR_MEMPTY // Return an empty vector
   }
 }
 
diff --git a/tests/evm_test.rs b/tests/evm_test.rs
index 5c88dff..6571da5 100644
--- a/tests/evm_test.rs
+++ b/tests/evm_test.rs
@@ -6,7 +6,7 @@ use rhoevm::modules::format::{hex_byte_string, strip_0x};
 
 //use rhoevm::modules::solvers::{with_solvers, Solver};
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, VM, W256};
+use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 const MAX_NUM_ITERATIONS: u32 = 1;
 
@@ -22,7 +22,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };