diff --git a/src/main/scala/ir/Statement.scala b/src/main/scala/ir/Statement.scala
index 8a8808b15..42a384eed 100644
--- a/src/main/scala/ir/Statement.scala
+++ b/src/main/scala/ir/Statement.scala
@@ -10,7 +10,7 @@ trait Statement extends Command {
   )
 }
 
-case class LocalAssign(var lhs: Variable, var rhs: Expr, val address: Option[Int] = None) extends Statement {
+case class LocalAssign(var lhs: Variable, var rhs: Expr, val label: Option[String] = None) extends Statement {
   //override def locals: Set[Variable] = rhs.locals + lhs
   override def modifies: Set[Global] = lhs match {
     case r: Register => Set(r)
@@ -20,7 +20,7 @@ case class LocalAssign(var lhs: Variable, var rhs: Expr, val address: Option[Int
   override def acceptVisit(visitor: Visitor): Statement = visitor.visitLocalAssign(this)
 }
 
-case class MemoryAssign(var lhs: Memory, var rhs: MemoryStore, val address: Option[Int] = None) extends Statement {
+case class MemoryAssign(var lhs: Memory, var rhs: MemoryStore, val label: Option[String] = None) extends Statement {
   override def modifies: Set[Global] = Set(lhs)
   //override def locals: Set[Variable] = rhs.locals
   override def toString: String = s"$lhs := $rhs"
diff --git a/src/main/scala/translating/BAPToIR.scala b/src/main/scala/translating/BAPToIR.scala
index 62c9e5ab4..73be03222 100644
--- a/src/main/scala/translating/BAPToIR.scala
+++ b/src/main/scala/translating/BAPToIR.scala
@@ -60,8 +60,8 @@ class BAPToIR(var program: BAPProgram, mainAddress: Int) {
   }
 
   private def translate(s: BAPStatement) = s match {
-    case b: BAPMemAssign   => MemoryAssign(b.lhs.toIR, b.rhs.toIR, b.address)
-    case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR, b.address)
+    case b: BAPMemAssign   => MemoryAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
+    case b: BAPLocalAssign => LocalAssign(b.lhs.toIR, b.rhs.toIR, Some(b.line))
     case _                 => throw new Exception("unsupported statement: " + s)
   }
 
diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala
index 3e3193833..5b76ebd3e 100644
--- a/src/main/scala/translating/IRToBoogie.scala
+++ b/src/main/scala/translating/IRToBoogie.scala
@@ -319,7 +319,7 @@ class IRToBoogie(var program: Program, var spec: Specification) {
 
   def translateBlock(b: Block): BBlock = {
     val cmds = (b.address match {
-      case Some(addr) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
+      case Some(addr) => List(getCaptureStateStatement(s"addr:${b.label}"))
       case _ => List.empty
     }) ++ (b.statements.flatMap(s => translate(s)) ++ b.jumps.flatMap(j => translate(j)))
 
@@ -379,8 +379,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
       val rhsGamma = m.rhs.toGamma
       val store = AssignCmd(List(lhs, lhsGamma), List(rhs, rhsGamma))
       val stateSplit = s match {
-        case MemoryAssign (_,_, Some(addr)) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
-        case LocalAssign(_,_, Some(addr)) => List(getCaptureStateStatement(s"addr:0x${addr.toHexString}"))
+        case MemoryAssign (_,_, Some(label)) => List(getCaptureStateStatement(s"${label}"))
+        case LocalAssign(_,_, Some(label)) => List(getCaptureStateStatement(s"${label}"))
         case _ => List.empty
       }
       if (lhs == stack) {