diff --git a/shared/src/main/scala/org/sireum/logika/Context.scala b/shared/src/main/scala/org/sireum/logika/Context.scala
index 506410b1..033893f7 100644
--- a/shared/src/main/scala/org/sireum/logika/Context.scala
+++ b/shared/src/main/scala/org/sireum/logika/Context.scala
@@ -107,18 +107,18 @@ object Context {
       return r
     }
 
-    def localMap(sm: HashMap[String, AST.Typed]): HashSMap[String, (ISZ[String], AST.Id, AST.Typed)] = {
-      var r = HashSMap.empty[String, (ISZ[String], AST.Id, AST.Typed)]
+    def localMap(sm: HashMap[String, AST.Typed]): HashSMap[String, (B, ISZ[String], AST.Id, AST.Typed)] = {
+      var r = HashSMap.empty[String, (B, ISZ[String], AST.Id, AST.Typed)]
       for (p <- params) {
         val (id, t) = p
-        r = r + id.value ~> ((name, id, t.subst(sm)))
+        r = r + id.value ~> ((T, name, id, t.subst(sm)))
       }
       for (x <- reads ++ modifies) {
         x.resOpt.get match {
           case res: AST.ResolvedInfo.LocalVar if !r.contains(res.id) =>
-            r = r + res.id ~> ((res.context, AST.Id(res.id, AST.Attr(x.posOpt)), x.typedOpt.get.subst(sm)))
+            r = r + res.id ~> ((res.isVal, res.context, AST.Id(res.id, AST.Attr(x.posOpt)), x.typedOpt.get.subst(sm)))
           case res: AST.ResolvedInfo.Var if !(res.isInObject || res.owner.isEmpty) && !r.contains("this") =>
-            r = r + "this" ~> ((name, AST.Id("this", AST.Attr(x.posOpt)), receiverTypeOpt.get))
+            r = r + "this" ~> ((T, name, AST.Id("this", AST.Attr(x.posOpt)), receiverTypeOpt.get))
           case _ =>
         }
       }
diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
index 8839524c..9583bd54 100644
--- a/shared/src/main/scala/org/sireum/logika/Logika.scala
+++ b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -918,6 +918,8 @@ import Util._
     (jps, eps, sps, cps, mps)
   }
 
+  @strictpure def isSymExe: B = config.mode == Config.VerificationMode.SymExe
+
   def zero(tipe: AST.Typed.Name, pos: Position): State.Value = {
     tipe match {
       case AST.Typed.z => return State.Value.Z(0, pos)
@@ -936,7 +938,7 @@ import Util._
       return s0
     }
     val pos = posOpt.get
-    if (config.mode != Config.VerificationMode.SymExe) {
+    if (!isSymExe) {
       val (s1, size) = s0.freshSym(AST.Typed.z, pos)
       val (s2, loCond) = s1.freshSym(AST.Typed.b, pos)
       val (s3, hiCond) = s2.freshSym(AST.Typed.b, pos)
@@ -1085,7 +1087,7 @@ import Util._
     if (!info.ast.isVal) {
       return None()
     }
-    AST.Util.constantInitOpt(info.ast) match {
+    AST.Util.constantInitOpt(info.ast.initOpt, info.ast.attr.typedOpt) match {
       case Some(exp) =>
         val r = evalExp(Split.Disabled, smt2, cache, rtCheck, s0, exp, reporter)
         assert(r.size == 1)
@@ -1298,6 +1300,16 @@ import Util._
           val (s1, v) = nameIntro(pos, s0, name :+ id, t, Some(pos))
           return (s1, v)
         case res: AST.ResolvedInfo.LocalVar =>
+          if (res.context.isEmpty) {
+            th.nameMap.get(ISZ(res.id)) match {
+              case Some(info: Info.LocalVar) =>
+                AST.Util.constantInitOpt(info.initOpt, info.typedOpt) match {
+                  case Some(init) => return evalExp(split, smt2, cache, rtCheck, s0, init, reporter)(0)
+                  case _ =>
+                }
+              case _ =>
+            }
+          }
           val (s1, r) = idIntro(pos, s0, res.context, res.id, t, None())
           return (s1, r)
         case res: AST.ResolvedInfo.Var =>
@@ -1405,7 +1417,7 @@ import Util._
         if (!rtCheck || !s0.ok) {
           return s0
         }
-        if (config.mode != Config.VerificationMode.SymExe) {
+        if (!isSymExe) {
           val tipe = value.tipe.asInstanceOf[AST.Typed.Name]
           val (s1, cond) = s0.freshSym(AST.Typed.b, pos)
           val s2 = s1.addClaims(ISZ(
@@ -2507,7 +2519,7 @@ import Util._
         }
         var localInMap = mctx.localInMap
         for (p <- mctx.localMap(typeSubstMap).entries) {
-          val (id, (ctx, _, t)) = p
+          val (id, (_, ctx, _, t)) = p
           val (s7, sym): (State, State.Value.Sym) = idIntro(pos, s1, ctx, id, t, None())
           localInMap = localInMap + id ~> sym
           s1 = s7
@@ -3684,7 +3696,7 @@ import Util._
                   posOpt: Option[Position], rwLocals: ISZ[AST.ResolvedInfo], reporter: Reporter): State = {
     val conclusion = State.Claim.Prop(T, sym)
     val pos = posOpt.get
-    if (config.mode != Config.VerificationMode.SymExe) {
+    if (!isSymExe) {
       Util.claimsToExpsLastOpt(jescmPlugins._4, pos, context.methodName, s0.claims :+ conclusion, th, F, config.atRewrite) match {
         case (pcs, Some(conc), _) =>
           val pcs2: HashSSet[AST.Exp] = if (rwLocals.nonEmpty) {
diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala
index f647cfc4..64f00e28 100644
--- a/shared/src/main/scala/org/sireum/logika/Util.scala
+++ b/shared/src/main/scala/org/sireum/logika/Util.scala
@@ -1994,7 +1994,7 @@ object Util {
       case Some(receiverType) =>
         val (s1, thiz) = idIntro(mctx.posOpt.get, s0, mctx.name, "this", receiverType, mctx.posOpt)
         localInMap = localInMap + "this" ~> thiz
-        s0 = s1.addClaim(State.Claim.Input(T, F, mctx.name, "this", thiz, thiz.pos))
+        s0 = if (!l.th.isMutable(receiverType)) s1 else s1.addClaim(State.Claim.Input(T, F, mctx.name, "this", thiz, thiz.pos))
         thisAdded = T
         for (p <- mctx.fieldVarMap(TypeChecker.emptySubstMap).entries) {
           val (id, (t, posOpt)) = p
@@ -2005,18 +2005,18 @@ object Util {
       case _ =>
     }
     for (v <- mctx.localMap(TypeChecker.emptySubstMap).values) {
-      val (mname, id, t) = v
+      val (isVal, mname, id, t) = v
       val posOpt = id.attr.posOpt
       if (id.value != "this") {
         val (s1, sym) = idIntro(posOpt.get, s0, mname, id.value, t, posOpt)
-        s0 = s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos))
+        s0 = if (isVal && !l.th.isMutable(t)) s1 else s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos))
         if (!isHelper) {
           s0 = assumeValueInv(l, smt2, cache, T, s0, sym, posOpt.get, reporter)
         }
         localInMap = localInMap + id.value ~> sym
       } else if (!thisAdded) {
         val (s1, sym) = idIntro(posOpt.get, s0, mname, id.value, t, mctx.posOpt)
-        s0 = s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos))
+        s0 = if (!l.th.isMutable(t)) s1 else s1.addClaim(State.Claim.Input(T, F, mname, id.value, sym, sym.pos))
         localInMap = localInMap + id.value ~> sym
         thisAdded = T
       }
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
index b4acce61..fb70012b 100644
--- a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
+++ b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
@@ -294,7 +294,7 @@ import InceptionPlugin._
         return emptyResult
       }
       val (status, nextFresh, claims, claim): (B, Z, ISZ[State.Claim], State.Claim) =
-        if (logika.config.mode == Config.VerificationMode.SymExe)
+        if (logika.isSymExe)
           logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
         else logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
       if (status && logika.config.detailedInfo) {