diff --git a/CHANGELOG.md b/CHANGELOG.md
index bb13db829..84679276c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Multiple solutions are allowed for a single symbolic expression
 - Aliasing works much better for symbolic and concrete addresses
 - Constant propagation for symbolic values
+- Add deployment code flag to the `equivalenceCheck` function
+- New simplification rule for reading a byte that is lower than destination offset in `copySlice`
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value
@@ -30,6 +32,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Better exponential simplification
 - Dumping of END states (.prop) files is now default for `--debug`
 - When cheatcode is missing, we produce a partial execution warning
+- The equivalence checker now is able to prove that an empty store is equivalent to a store with all slots initialized to 0.
+
 
 ## Changed
 - Warnings now lead printing FAIL. This way, users don't accidentally think that
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
index b38bfa4e7..7ca6067fd 100644
--- a/src/EVM/Expr.hs
+++ b/src/EVM/Expr.hs
@@ -243,6 +243,9 @@ readByte i@(Lit x) (WriteWord (Lit idx) val src)
            (Lit _) -> indexWord (Lit $ x - idx) val
            _ -> IndexWord (Lit $ x - idx) val
     else readByte i src
+-- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from dst
+readByte i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x =
+  readByte i dst
 readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst)
   = if x - dstOffset < size
     then readByte (Lit $ x - (dstOffset - srcOffset)) src
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index 0128c5fd3..b2d98684c 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -394,6 +394,7 @@ solcRuntime contract src = do
       Just (Contracts sol, _, _) -> pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.runtimeCode)
       Nothing -> internalError $ "unable to parse solidity output:\n" <> (T.unpack json)
 
+
 functionAbi :: Text -> IO Method
 functionAbi f = do
   json <- solc Solidity ("contract ABI { function " <> f <> " public {}}")
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 10fe1d037..aa2471b27 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -687,8 +687,9 @@ equivalenceCheck
   -> ByteString
   -> VeriOpts
   -> (Expr Buf, [Prop])
+  -> Bool
   -> m ([EquivResult], [Expr End])
-equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
+equivalenceCheck solvers bytecodeA bytecodeB opts calldata create = do
   conf <- readConfig
   case bytecodeA == bytecodeB of
     True -> liftIO $ do
@@ -706,7 +707,7 @@ equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
     getBranches :: ByteString -> m [Expr End]
     getBranches bs = do
       let bytecode = if BS.null bs then BS.pack [0] else bs
-      prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing False
+      prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create
       expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr
       let simpl = if opts.simp then (Expr.simplify expr) else expr
       pure $ flattenExpr simpl
@@ -844,7 +845,7 @@ equivalenceCheck' solvers branchesA branchesB = do
         -- TODO: is this sound? do we need a more sophisticated nonce representation?
         noncesDiffer = PBool (ac.nonce /= bc.nonce)
         storesDiffer = case (ac.storage, bc.storage) of
-          (ConcreteStore as, ConcreteStore bs) -> PBool $ as /= bs
+          (ConcreteStore as, ConcreteStore bs) | not (as == Map.empty || bs == Map.empty) -> PBool $ as /= bs
           (as, bs) -> if as == bs then PBool False else as ./= bs
       in balsDiffer .|| storesDiffer .|| noncesDiffer
 
diff --git a/test/test.hs b/test/test.hs
index 82da7c908..e4a0b2048 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -3747,9 +3747,29 @@ tests = testGroup "hevm"
           }
           |]
         withSolvers Z3 3 1 Nothing $ \s -> do
-          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
+          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False
           assertBoolM "Must have a difference" (any isCex res)
       ,
+      test "implicit-constructor" $ do
+        Just initA <- solidity "C"
+          [i|
+            contract C {
+              uint x;
+            }
+          |]
+        Just initB <- solidity "C"
+          [i|
+            contract C {
+              uint x;
+              constructor() {
+                x = 0;
+              }
+            }
+          |]
+        withSolvers Z3 3 1 Nothing $ \s -> do
+          (res, _) <- equivalenceCheck s initA initB defaultVeriOpts (mkCalldata Nothing []) True
+          assertEqualM "Must have no difference" [Qed ()] res
+      ,
       test "eq-sol-exp-qed" $ do
         Just aPrgm <- solcRuntime "C"
           [i|
@@ -3772,7 +3792,7 @@ tests = testGroup "hevm"
             }
           |]
         withSolvers Z3 3 1 Nothing $ \s -> do
-          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
+          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False
           assertEqualM "Must have no difference" [Qed ()] res
       ,
       test "eq-balance-differs" $ do
@@ -3803,7 +3823,7 @@ tests = testGroup "hevm"
             }
           |]
         withSolvers Z3 3 1 Nothing $ \s -> do
-          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
+          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False
           assertBoolM "Must differ" (all isCex res)
       ,
       -- TODO: this fails because we don't check equivalence of deployed contracts
@@ -3864,7 +3884,7 @@ tests = testGroup "hevm"
             }
           |]
         withSolvers Z3 3 1 Nothing $ \s -> do
-          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
+          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False
           assertBoolM "Must differ" (all isCex res)
       ,
       test "eq-unknown-addr" $ do
@@ -3888,7 +3908,7 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 1 Nothing $ \s -> do
           let cd = mkCalldata (Just (Sig "a(address,address)" [AbiAddressType, AbiAddressType])) []
-          (res,_) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd
+          (res,_) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd False
           assertEqualM "Must be different" (any isCex res) True
       ,
       test "eq-sol-exp-cex" $ do
@@ -3913,7 +3933,7 @@ tests = testGroup "hevm"
               }
           |]
         withSolvers Bitwuzla 3 1 Nothing $ \s -> do
-          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
+          (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False
           assertEqualM "Must be different" (any isCex res) True
       , test "eq-all-yul-optimization-tests" $ do
         let opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 20, loopHeuristic = Naive }
@@ -4126,7 +4146,7 @@ tests = testGroup "hevm"
           Just bPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredBSym
           procs <- liftIO $ getNumProcessors
           withSolvers CVC5 (unsafeInto procs) 1 (Just 100) $ \s -> do
-            (res, _) <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing [])
+            (res, _) <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing []) False
             end <- liftIO $ getCurrentTime
             case any isCex res of
               False -> liftIO $ do