diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1077240d1..f6eaebe54 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,7 +46,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   print some warnings related to zero-address dereference and to print `hemv test`'s
   output in case of failure
 - Simple test cases for the CLI
-- Allow limiting the branch depth and width limitation via --max-depth and --max-width
+- Allow limiting the branch depth and width limitation via --max-depth and --max-width.
+  This limitation takes into account all branchings, including ones that
+  are later simplified away
 - When there are zero solutions to a multi-solution query it means that the
   currently executed branch is in fact impossible. In these cases, unwind all
   frames and return a Revert with empty returndata.
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 2179b1dd7..22000bb3e 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -373,9 +373,6 @@ interpret fetcher iterConf vm =
 
         case q of
           PleaseAskSMT cond preconds continue -> do
-            let
-              -- no concretiziation here, or we may lose information
-              simpProps = Expr.simplifyProps ((cond ./= Lit 0):preconds)
             case Expr.concKeccakSimpExpr cond of
               -- is the condition concrete?
               Lit c ->
@@ -405,11 +402,12 @@ interpret fetcher iterConf vm =
                     -- ask the smt solver about the loop condition
                     performQuery
                   _ -> do
-                    (r, vm') <- case simpProps of
+                    (r, vm') <- case Expr.concKeccakProps ((cond ./= Lit 0):preconds) of
                       -- if we can statically determine unsatisfiability then we skip exploring the jump
                       [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm
+                      [] -> liftIO $ stToIO $ runStateT (continue (Case True)) vm
                       -- otherwise we explore both branches
-                      _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm
+                      _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm {exploreDepth = vm.exploreDepth+1}
                     interpret fetcher iterConf vm' (k r)
           _ -> performQuery
 
diff --git a/test/test.hs b/test/test.hs
index f2042b2ad..c5a8c7471 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1582,7 +1582,7 @@ tests = testGroup "hevm"
           assertEqualM "number of qed-s" 1 numQeds
       -- below we don't hit the limit of the depth of the symbolic execution tree
       , testCase "limit-num-explore-no-hit-limit" $ do
-        let conf = testEnv.config {maxDepth = Just 4}
+        let conf = testEnv.config {maxDepth = Just 7}
         let myTestEnv :: Env = (testEnv :: Env) {config = conf :: Config}
         runEnv myTestEnv $ do
           Just c <- solcRuntime "C"