diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala
index 0349082aa..fe275c0cd 100644
--- a/src/main/scala/analysis/Analysis.scala
+++ b/src/main/scala/analysis/Analysis.scala
@@ -124,13 +124,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /**
-    * Controls the pool of stack regions. Each pool is unique to a function.
-    * If the offset has already been defined in the context of the function, then the same region is returned.
-    *
-    * @param expr   : the offset
-    * @param parent : the function entry node
-    * @return the stack region corresponding to the offset
-    */
+   * Controls the pool of stack regions. Each pool is unique to a function.
+   * If the offset has already been defined in the context of the function, then the same region is returned.
+   *
+   * @param expr   : the offset
+   * @param parent : the function entry node
+   * @return the stack region corresponding to the offset
+   */
   def poolMaster(expr: BitVecLiteral, parent: CfgFunctionEntryNode): StackRegion = {
     val stackPool = stackMap.getOrElseUpdate(parent, mutable.HashMap())
     if (stackPool.contains(expr)) {
@@ -161,17 +161,18 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     buffers
   }
 
-  /** The lattice of abstract values.
-    */
-  val powersetLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
+  val regionLattice: PowersetLattice[MemoryRegion] = PowersetLattice()
 
-  /** The lattice of abstract states.
+  /**
+    * Lifted memory region lattice, with new bottom element representing "unreachable".
     */
-  val lattice: MapLattice[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] = MapLattice(powersetLattice)
+  val liftedLattice: LiftLattice[Set[MemoryRegion], PowersetLattice[MemoryRegion]] = LiftLattice(regionLattice)
+
+  val lattice: MapLattice[CfgNode, LiftedElement[Set[MemoryRegion]], LiftLattice[Set[MemoryRegion], PowersetLattice[MemoryRegion]]] = MapLattice(liftedLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
-  val first: Set[CfgNode] = domain.collect { case n: CfgFunctionEntryNode if n.predIntra.isEmpty => n }
+  val first: Set[CfgNode] = cfg.funEntries.toSet
 
   private val stackPointer = Register("R31", BitVecType(64))
   private val linkRegister = Register("R30", BitVecType(64))
@@ -232,6 +233,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
                 env // we cannot evaluate this to a concrete value, we need VSA for this
             }
         }
+      // we cannot evaluate this to a concrete value, we need VSA for this
       case _ =>
         Logger.debug(s"type: ${exp.getClass} $exp\n")
         throw new Exception("Unknown type")
@@ -239,7 +241,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
   }
 
   /** Transfer function for state lattice elements.
-    */
+   */
   def localTransfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = n match {
     case cmd: CfgCommandNode =>
       cmd.data match {
@@ -247,7 +249,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
           if (directCall.target.name == "malloc") {
             evaluateExpression(mallocVariable, constantProp(n)) match {
               case Some(b: BitVecLiteral) =>
-                lattice.sublattice.lub(s, Set(HeapRegion(nextMallocCount())))
+                regionLattice.lub(s, Set(HeapRegion(nextMallocCount(), b)))
               case None => s
             }
           } else {
@@ -258,46 +260,13 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
             return s
           }
           val result = eval(memAssign.rhs.index, s, cmd)
-          /*
-          don't modify the IR in the middle of the analysis like this, also this produces a lot of incorrect results
-          result.collectFirst({
-            case StackRegion(name, _, _, _) =>
-              memAssign.rhs = MemoryStore(
-                Memory(name,
-                  memAssign.rhs.mem.addressSize,
-                  memAssign.rhs.mem.valueSize),
-                memAssign.rhs.index,
-                memAssign.rhs.value, memAssign.rhs.endian,
-                memAssign.rhs.size
-              )
-            case DataRegion(name, _, _, _) =>
-              memAssign.rhs = MemoryStore(
-                Memory(name, memAssign.rhs.mem.addressSize, memAssign.rhs.mem.valueSize),
-                memAssign.rhs.index,
-                memAssign.rhs.value,
-                memAssign.rhs.endian,
-                memAssign.rhs.size
-              )
-            case _ =>
-          })
-          */
-          lattice.sublattice.lub(s, result)
+          regionLattice.lub(s, result)
         case localAssign: LocalAssign =>
           var m = s
           unwrapExpr(localAssign.rhs).foreach {
             case memoryLoad: MemoryLoad =>
               val result = eval(memoryLoad.index, s, cmd)
-              /*
-              don't modify the IR in the middle of the analysis like this, this also produces incorrect results
-              result.collectFirst({
-                case StackRegion(name, _, _, _) =>
-                  memoryLoad.mem = Memory(name, memoryLoad.mem.addressSize, memoryLoad.mem.valueSize)
-                case DataRegion(name, _, _, _) =>
-                  memoryLoad.mem = Memory(name, memoryLoad.mem.addressSize, memoryLoad.mem.valueSize)
-                case _ =>
-              })
-              */
-              m = lattice.sublattice.lub(m, result)
+              m = regionLattice.lub(m, result)
             case _ => m
           }
           m
@@ -306,10 +275,7 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
     case _ => s // ignore other kinds of nodes
   }
 
-  /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
-    */
-  def transfer(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
-
+  def transferUnlifted(n: CfgNode, s: Set[MemoryRegion]): Set[MemoryRegion] = localTransfer(n, s)
 }
 
 class MemoryRegionAnalysisSolver(
@@ -320,4 +286,15 @@ class MemoryRegionAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]]
 ) extends MemoryRegionAnalysis(cfg, globals, globalOffsets, subroutines, constantProp)
     with IntraproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]]
\ No newline at end of file
+    with Analysis[Map[CfgNode, LiftedElement[Set[MemoryRegion]]]]
+    with WorklistFixpointSolverWithReachability[CfgNode, Set[MemoryRegion], PowersetLattice[MemoryRegion]] {
+
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Set[MemoryRegion]]]): LiftedElement[Set[MemoryRegion]] = {
+    n match {
+      // function entry nodes are always reachable as this is intraprocedural
+      case _: CfgFunctionEntryNode => liftedLattice.lift(regionLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/analysis/Cfg.scala b/src/main/scala/analysis/Cfg.scala
index dfaa113dd..b5a49f98c 100644
--- a/src/main/scala/analysis/Cfg.scala
+++ b/src/main/scala/analysis/Cfg.scala
@@ -203,6 +203,7 @@ class ProgramCfg:
 
   var startNode: CfgFunctionEntryNode = _
   var nodes: mutable.Set[CfgNode] = mutable.Set()
+  var funEntries: mutable.Set[CfgFunctionEntryNode] = mutable.Set()
 
   /** Inline edges are for connecting an intraprocedural cfg with a copy of another procedure's intraprocedural cfg
     * which is placed inside this one. They are considered interprocedural edges, and will not be followed if the caller
@@ -414,6 +415,7 @@ class ProgramCfgFactory:
     val funcExitNode: CfgFunctionExitNode = CfgFunctionExitNode(proc)
     cfg.nodes += funcEntryNode
     cfg.nodes += funcExitNode
+    cfg.funEntries += funcEntryNode
 
     procToCfg += (proc -> (funcEntryNode, funcExitNode))
     callToNodes += (funcEntryNode -> mutable.Set())
diff --git a/src/main/scala/analysis/Lattice.scala b/src/main/scala/analysis/Lattice.scala
index e2379815c..6f9cb5f41 100644
--- a/src/main/scala/analysis/Lattice.scala
+++ b/src/main/scala/analysis/Lattice.scala
@@ -32,6 +32,45 @@ class PowersetLattice[A] extends Lattice[Set[A]] {
   def lub(x: Set[A], y: Set[A]): Set[A] = x.union(y)
 }
 
+trait LiftedElement[+T]
+case class Lift[T](el: T) extends LiftedElement[T] {
+  override def toString = s"Lift($el)"
+}
+case object LiftedBottom extends LiftedElement[Nothing] {
+  override def toString = "LiftBot"
+}
+/**
+ * The lift lattice for `sublattice`.
+ * Supports implicit lifting and unlifting.
+ */
+class LiftLattice[T, +L <: Lattice[T]](val sublattice: L) extends Lattice[LiftedElement[T]] {
+
+  val bottom: LiftedElement[T] = LiftedBottom
+
+  def lub(x: LiftedElement[T], y: LiftedElement[T]): LiftedElement[T] =
+    (x, y) match {
+      case (LiftedBottom, t) => t
+      case (t, LiftedBottom) => t
+      case (Lift(a), Lift(b)) => Lift(sublattice.lub(a, b))
+    }
+
+  /**
+   * Lift elements of the sublattice to this lattice.
+   * Note that this method is declared as implicit, so the conversion can be done automatically.
+   */
+  def lift(x: T): LiftedElement[T] = Lift(x)
+
+  /**
+   * Un-lift elements of this lattice to the sublattice.
+   * Throws an IllegalArgumentException if trying to unlift the bottom element
+   * Note that this method is declared as implicit, so the conversion can be done automatically.
+   */
+  def unlift(x: LiftedElement[T]): T = x match {
+    case Lift(s) => s
+    case LiftedBottom => throw new IllegalArgumentException("Cannot unlift bottom")
+  }
+}
+
 trait FlatElement[+T]
 case class FlatEl[T](el: T) extends FlatElement[T]
 case object Top extends FlatElement[Nothing]
diff --git a/src/main/scala/analysis/MemoryModelMap.scala b/src/main/scala/analysis/MemoryModelMap.scala
index 87456b54d..a33b7b6af 100644
--- a/src/main/scala/analysis/MemoryModelMap.scala
+++ b/src/main/scala/analysis/MemoryModelMap.scala
@@ -44,27 +44,29 @@ class MemoryModelMap {
     }
   }
 
-  def convertMemoryRegions(memoryRegions: Map[CfgNode, Set[MemoryRegion]], externalFunctions: Map[BigInt, String]): Unit = {
+  def convertMemoryRegions(memoryRegions: Map[CfgNode, LiftedElement[Set[MemoryRegion]]], externalFunctions: Map[BigInt, String]): Unit = {
     // map externalFunctions name, value to DataRegion(name, value) and then sort by value
     val externalFunctionRgns = externalFunctions.map((offset, name) => DataRegion(name, BitVecLiteral(offset, 64)))
 
     // get all function exit node
     val exitNodes = memoryRegions.keys.collect { case e: CfgFunctionExitNode => e }
     exitNodes.foreach(exitNode =>
-      val node = memoryRegions(exitNode)
+      memoryRegions(exitNode) match {
+        case Lift(node) =>
+          // for each function exit node we get the memory region and add it to the mapping
+          val stackRgns = node.collect { case r: StackRegion => r }.toList.sortBy(_.start.value)
+          val dataRgns = node.collect { case r: DataRegion => r }
 
-      // for each function exit node we get the memory region and add it to the mapping
-      val stackRgns = node.collect { case r: StackRegion => r }.toList.sortBy(_.start.value)
-      val dataRgns = node.collect { case r: DataRegion => r }
+          // add externalFunctionRgn to dataRgns and sort by value
+          val allDataRgns = (dataRgns ++ externalFunctionRgns).toList.sortBy(_.start.value)
 
-      // add externalFunctionRgn to dataRgns and sort by value
-      val allDataRgns = (dataRgns ++ externalFunctionRgns).toList.sortBy(_.start.value)
+          allStacks(exitNode.data.name) = stackRgns
 
-      allStacks(exitNode.data.name) = stackRgns
-
-      for (dataRgn <- allDataRgns) {
-        add(dataRgn.start.value, dataRgn)
-      }
+          for (dataRgn <- allDataRgns) {
+            add(dataRgn.start.value, dataRgn)
+          }
+        case LiftedBottom =>
+    }
     )
   }
 
@@ -123,8 +125,8 @@ class StackRegion(override val regionIdentifier: String, val start: BitVecLitera
   }
 }
 
-class HeapRegion(override val regionIdentifier: String) extends MemoryRegion {
-  override def toString: String = s"Heap($regionIdentifier)"
+class HeapRegion(override val regionIdentifier: String, val size: BitVecLiteral) extends MemoryRegion {
+  override def toString: String = s"Heap($regionIdentifier, $size)"
   override def hashCode(): Int = regionIdentifier.hashCode()
   override def equals(obj: Any): Boolean = obj match {
     case h: HeapRegion => h.regionIdentifier == regionIdentifier
diff --git a/src/main/scala/analysis/UtilMethods.scala b/src/main/scala/analysis/UtilMethods.scala
index 7a4f44137..402076ee5 100644
--- a/src/main/scala/analysis/UtilMethods.scala
+++ b/src/main/scala/analysis/UtilMethods.scala
@@ -25,6 +25,7 @@ def evaluateExpression(exp: Expr, constantPropResult: Map[Variable, FlatElement[
             case BVSUB => Some(BitVectorEval.smt_bvsub(l, r))
             case BVASHR => Some(BitVectorEval.smt_bvashr(l, r))
             case BVCOMP => Some(BitVectorEval.smt_bvcomp(l, r))
+            case BVCONCAT => Some(BitVectorEval.smt_concat(l, r))
             case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op)
           }
         case _ => None
diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala
index 4a8f3342d..a09a1c5f3 100644
--- a/src/main/scala/analysis/VSA.scala
+++ b/src/main/scala/analysis/VSA.scala
@@ -41,7 +41,9 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   val mapLattice: MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]] = MapLattice(powersetLattice)
 
-  val lattice: MapLattice[CfgNode, Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = MapLattice(mapLattice)
+  val liftedLattice: LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type] = LiftLattice(mapLattice)
+
+  val lattice: MapLattice[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]], LiftLattice[Map[Variable | MemoryRegion, Set[Value]], mapLattice.type]] = MapLattice(liftedLattice)
 
   val domain: Set[CfgNode] = cfg.nodes.toSet
 
@@ -102,6 +104,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
     Logger.debug(s"eval: $cmd")
     Logger.debug(s"state: $s")
     Logger.debug(s"node: $n")
+    var m = s
     cmd match
       case localAssign: LocalAssign =>
         localAssign.rhs match
@@ -111,19 +114,23 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                 // this is an exception to the rule and only applies to data regions
                 evaluateExpression(memoryLoad.index, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    val m = s + (r -> Set(getValueType(bitVecLiteral)))
-                    m + (localAssign.lhs -> m(r))
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m = m + (localAssign.lhs -> m(r))
+                    m
                   case None =>
-                    s + (localAssign.lhs -> s(r))
+                    m = m + (localAssign.lhs -> m(r))
+                    m
               case None =>
                 Logger.warn("could not find region for " + localAssign)
-                s
+                m
           case e: Expr =>
             evaluateExpression(e, constantProp(n)) match {
-              case Some(bv: BitVecLiteral) => s + (localAssign.lhs -> Set(getValueType(bv)))
+              case Some(bv: BitVecLiteral) =>
+                m = m + (localAssign.lhs -> Set(getValueType(bv)))
+                m
               case None =>
                 Logger.warn("could not evaluate expression" + e)
-                s
+                m
             }
       case memAssign: MemoryAssign =>
         memAssign.rhs.index match
@@ -134,27 +141,29 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
                 val storeValue = memAssign.rhs.value
                 evaluateExpression(storeValue, constantProp(n)) match
                   case Some(bitVecLiteral: BitVecLiteral) =>
-                    s + (r -> Set(getValueType(bitVecLiteral)))
-                  /*
-                // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
-                case variable: Variable =>
-                  s + (r -> s(variable))
-                  */
+                    m = m + (r -> Set(getValueType(bitVecLiteral)))
+                    m
+                    /*
+                  // TODO constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address
+                  case variable: Variable =>
+                    s + (r -> s(variable))
+                    */
                   case None =>
                     storeValue.match {
                       case v: Variable =>
-                        s + (r -> s(v))
+                        m = m + (r -> m(v))
+                        m
                       case _ =>
                         Logger.warn(s"Too Complex: $storeValue") // do nothing
-                        s
+                        m
                     }
               case None =>
                 Logger.warn("could not find region for " + memAssign)
-                s
+                m
           case _ =>
-            s
+            m
       case _ =>
-        s
+        m
   }
 
   /** Transfer function for state lattice elements.
@@ -173,7 +182,7 @@ trait ValueSetAnalysis(cfg: ProgramCfg,
 
   /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
     */
-  def transfer(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
+  def transferUnlifted(n: CfgNode, s: Map[Variable | MemoryRegion, Set[Value]]): Map[Variable | MemoryRegion, Set[Value]] = localTransfer(n, s)
 }
 
 class ValueSetAnalysisSolver(
@@ -186,4 +195,15 @@ class ValueSetAnalysisSolver(
     constantProp: Map[CfgNode, Map[Variable, FlatElement[BitVecLiteral]]],
 ) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp)
     with InterproceduralForwardDependencies
-    with SimpleMonotonicSolver[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]]
+    with Analysis[Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]]
+    with WorklistFixpointSolverWithReachability[CfgNode, Map[Variable | MemoryRegion, Set[Value]], MapLattice[Variable | MemoryRegion, Set[Value], PowersetLattice[Value]]] {
+
+  override def funsub(n: CfgNode, x: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]]): LiftedElement[Map[Variable | MemoryRegion, Set[Value]]] = {
+    n match {
+      // function entry nodes are always reachable as this is intraprocedural
+      case _: CfgFunctionEntryNode => liftedLattice.lift(mapLattice.bottom)
+      // all other nodes are processed with join+transfer
+      case _ => super.funsub(n, x)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/analysis/solvers/FixPointSolver.scala b/src/main/scala/analysis/solvers/FixPointSolver.scala
index f86f1f260..aa4e52d5c 100644
--- a/src/main/scala/analysis/solvers/FixPointSolver.scala
+++ b/src/main/scala/analysis/solvers/FixPointSolver.scala
@@ -48,6 +48,27 @@ trait MapLatticeSolver[N, T, L <: Lattice[T]] extends LatticeSolver[Map[N, T]] w
     val states = indep(n).map(o(_))
     states.foldLeft(lattice.sublattice.bottom)((acc, pred) => lattice.sublattice.lub(acc, pred))
 
+/**
+ * Base trait for solvers for map lattices with lifted co-domains.
+ * @tparam N type of the elements in the map domain.
+ */
+trait MapLiftLatticeSolver[N, T, L <: Lattice[T]] extends MapLatticeSolver[N, LiftedElement[T], LiftLattice[T, L]] with Dependencies[N] {
+
+  val lattice: MapLattice[N, LiftedElement[T], LiftLattice[T, L]]
+
+  /**
+   * The transfer function for the sub-sub-lattice.
+   */
+  def transferUnlifted(n: N, s: T): T
+
+  override def transfer(n: N, s: LiftedElement[T]): LiftedElement[T] = {
+    s match {
+      case LiftedBottom => LiftedBottom // unreachable as input implied unreachable at output
+      case Lift(a) => lattice.sublattice.lift(transferUnlifted(n, a))
+    }
+  }
+}
+
 /** An abstract worklist algorithm.
   *
   * @tparam N
@@ -163,6 +184,25 @@ trait SimpleWorklistFixpointSolver[N, T, L <: Lattice[T]] extends WorklistFixpoi
     run(domain)
     x
 
+/**
+ * The worklist-based fixpoint solver with reachability.
+ *
+ * This solver works for map lattices with lifted co-domains, where the extra bottom element typically represents "unreachable".
+ */
+trait WorklistFixpointSolverWithReachability[N, T, L <: Lattice[T]] extends WorklistFixpointSolver[N, LiftedElement[T], LiftLattice[T, L]] with MapLiftLatticeSolver[N, T, L] {
+
+  /**
+   * The start locations, used as the initial contents of the worklist.
+   */
+  val first: Set[N]
+
+  def analyze(): Map[N, LiftedElement[T]] = {
+    x = lattice.bottom
+    run(first)
+    x
+  }
+}
+
 /** A pushDown worklist-based fixpoint solvers. Pushes the results of the analysis one node down. This is used to have
   * the results of the pred node in the current node. ie. NODE 1: R0 = 69551bv64 RESULT LATTICE = {} NODE 2: R0 =
   * MemLoad[R0 + 54bv64] RESULT LATTICE = {R0 = 69551bv64} NODE 3: R1 = 0bv64 RESULT LATTICE = {R0 = TOP} ...
@@ -191,7 +231,6 @@ trait PushDownWorklistFixpointSolver[N, T, L <: Lattice[T]] extends MapLatticeSo
   }
 
   def process(n: N): Unit =
-    //val y = funsub(n, x, intra)
     val xn = x(n)
     val y = transfer(n, xn)
 
diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala
index 3dbc4d07c..dd4173871 100644
--- a/src/main/scala/util/RunUtils.scala
+++ b/src/main/scala/util/RunUtils.scala
@@ -22,7 +22,7 @@ import util.Logger
 import scala.collection.mutable
 
 object RunUtils {
-  var memoryRegionAnalysisResults: Map[CfgNode, Set[MemoryRegion]] = Map()
+  var memoryRegionAnalysisResults: Map[CfgNode, LiftedElement[Set[MemoryRegion]]] = Map()
 
   // ids reserved by boogie
   val reserved: Set[String] = Set("free")
@@ -166,7 +166,7 @@ object RunUtils {
 
     Logger.info("[!] Running VSA")
     val vsaSolver = ValueSetAnalysisSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult)
-    val vsaResult = vsaSolver.analyze()
+    val vsaResult: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]] = vsaSolver.analyze()
 
     config.analysisDotPath.foreach(s => writeToFile(cfg.toDot(Output.labeler(vsaResult, true), Output.dotIder), s"${s}_vsa$iteration.dot"))
     config.analysisResultsPath.foreach(s => writeToFile(printAnalysisResults(cfg, vsaResult, iteration), s"${s}_vsa$iteration.txt"))
@@ -267,7 +267,7 @@ object RunUtils {
 
   def resolveCFG(
       cfg: ProgramCfg,
-      valueSets: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]],
+      valueSets: Map[CfgNode, LiftedElement[Map[Variable | MemoryRegion, Set[Value]]]],
       IRProgram: Program
   ): (Program, Boolean) = {
     var modified: Boolean = false
@@ -323,27 +323,31 @@ object RunUtils {
               // We want to replace all possible indirect calls based on this CFG, before regenerating it from the IR
               return
             }
-            val valueSet = valueSets(n)
-            val targetNames = resolveAddresses(valueSet(indirectCall.target)).map(_.name).toList.sorted
-            val targets = targetNames.map(name => IRProgram.procedures.filter(_.name.equals(name)).head)
-            if (targets.size == 1) {
-              modified = true
-              val newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
-              block.jump = newCall
-            } else if (targets.size > 1) {
-              modified = true
-              val procedure = c.parent.data
-              val newBlocks = ArrayBuffer[Block]()
-              for (t <- targets) {
-                val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
-                val newLabel: String = block.label + t.name
-                val directCall = DirectCall(t, indirectCall.returnTarget)
-                newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+            valueSets(n) match {
+              case Lift(valueSet) =>
+                val targetNames = resolveAddresses(valueSet(indirectCall.target)).map(_.name).toList.sorted
+                val targets = targetNames.map(name => IRProgram.procedures.filter(_.name.equals(name)).head)
+
+                if (targets.size == 1) {
+                  modified = true
+                  val newCall = DirectCall(targets.head, indirectCall.returnTarget, indirectCall.label)
+                  block.jump = newCall
+                } else if (targets.size > 1) {
+                  modified = true
+                  val procedure = c.parent.data
+                  val newBlocks = ArrayBuffer[Block]()
+                  for (t <- targets) {
+                    val assume = Assume(BinaryExpr(BVEQ, indirectCall.target, BitVecLiteral(t.address.get, 64)))
+                    val newLabel: String = block.label + t.name
+                    val directCall = DirectCall(t, indirectCall.returnTarget)
+                    newBlocks.append(Block(newLabel, None, ArrayBuffer(assume), directCall))
+                  }
+                  procedure.blocks.addAll(newBlocks)
+                  val newCall = GoTo(newBlocks, indirectCall.label)
+                  block.jump = newCall
+                }
+              case LiftedBottom =>
               }
-              procedure.blocks.addAll(newBlocks)
-              val newCall = GoTo(newBlocks, indirectCall.label)
-              block.jump = newCall
-            }
           case _ =>
       case _ =>
     }
diff --git a/src/test/scala/MemoryRegionAnalysisMiscTest.scala b/src/test/scala/MemoryRegionAnalysisMiscTest.scala
index 93cad362e..a25061293 100644
--- a/src/test/scala/MemoryRegionAnalysisMiscTest.scala
+++ b/src/test/scala/MemoryRegionAnalysisMiscTest.scala
@@ -1,9 +1,9 @@
-import analysis.{CfgNode, MemoryRegion}
+import analysis.{CfgNode, LiftedElement, MemoryRegion}
 import org.scalatest.Inside.inside
 import org.scalatest.*
 import org.scalatest.funsuite.*
 import util.RunUtils
-import util.{BASILConfig, ILLoadingConfig, BoogieGeneratorConfig, StaticAnalysisConfig, BoogieMemoryAccessMode}
+import util.{BASILConfig, BoogieGeneratorConfig, BoogieMemoryAccessMode, ILLoadingConfig, StaticAnalysisConfig}
 
 import java.io.{File, OutputStream, PrintStream, PrintWriter}
 class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
@@ -15,7 +15,7 @@ class MemoryRegionAnalysisMiscTest extends AnyFunSuite with OneInstancePerTest {
   def runMain(name: String, dump: Boolean = false): Unit = {
     var expected = ""
     var actual = ""
-    var output: Map[CfgNode, Set[MemoryRegion]] = Map()
+    var output: Map[CfgNode, LiftedElement[Set[MemoryRegion]]] = Map()
     RunUtils.loadAndTranslate(
       BASILConfig(
         loading = ILLoadingConfig(