Made sure val for constant invariant.

sireum · Sep 15, 2023 · a535c39 · a535c39
1 parent 194454d
commit a535c39
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -1302,7 +1302,7 @@ 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 && context.methodName.nonEmpty) {
+          if (res.isVal && res.context.isEmpty && context.methodName.nonEmpty) {
             th.nameMap.get(ISZ(res.id)) match {
               case Some(info: Info.LocalVar) =>
                 AST.Util.constantInitOpt(info.initOpt, info.typedOpt) match {