diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala
index 52e50b162d..6a6132b2b4 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala
@@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir.oper.TlaActionOper
-import at.forsyte.apalache.tla.lir.{NameEx, OperEx}
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
+import at.forsyte.apalache.tla.lir.{NameEx, OperEx, TlaType1}
+import at.forsyte.apalache.tla.types.tla
 
 /**
  * Rename x' to NameEx("x'"). We only consider the case when prime is applied to a variable.
@@ -21,8 +21,8 @@ class PrimeRule extends RewritingRule {
 
   override def apply(state: SymbState): SymbState = {
     state.ex match {
-      case OperEx(TlaActionOper.prime, NameEx(name)) =>
-        state.setRex(NameEx(name + "'"))
+      case OperEx(TlaActionOper.prime, nEx @ NameEx(name)) =>
+        state.setRex(tla.name(name + "'", TlaType1.fromTypeTag(nEx.typeTag)))
 
       case _ =>
         throw new RewriterException("Prime operator is only implemented for variables", state.ex)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
index 66a55f9742..dab6a4474d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
@@ -2,7 +2,6 @@ package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir.NameEx
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
 import at.forsyte.apalache.tla.pp.TlaInputError
 import com.typesafe.scalalogging.LazyLogging
 
@@ -29,7 +28,7 @@ class SubstRule extends RewritingRule with LazyLogging {
       case NameEx(x) =>
         if (state.binding.contains(x)) {
           val cell = state.binding(x)
-          state.setRex(NameEx(cell.toString))
+          state.setRex(cell.toBuilder)
         } else {
           logger.error("This error may show up when CONSTANTS are not initialized.")
           logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html")
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
index 445cc295b5..b741f7255f 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
@@ -2,18 +2,17 @@ package at.forsyte.apalache.tla.bmcmt
 
 import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt.SymbStateRewriter.Continue
-import at.forsyte.apalache.tla.lir.{IntT1, NameEx}
-import at.forsyte.apalache.tla.lir.convenience._
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
+import at.forsyte.apalache.tla.lir.IntT1
+import at.forsyte.apalache.tla.types.tla
 
 trait TestSymbStateRewriterAction extends RewriterBase {
   test("""x' is rewritten to the binding of x'""") { rewriterType: SMTEncoding =>
     val rewriter = create(rewriterType)
     arena.appendCell(IntT1) // the type finder is strict about unassigned types, so let's create a cell for x'
-    val state = new SymbState(tla.prime(NameEx("x")), arena, Binding("x'" -> arena.topCell))
+    val state = new SymbState(tla.prime(tla.name("x", IntT1)), arena, Binding("x'" -> arena.topCell))
     rewriter.rewriteOnce(state) match {
       case Continue(next) =>
-        assert(next.ex == NameEx("x'"))
+        assert(next.ex == tla.name("x'", IntT1).build)
 
       case _ =>
         fail("Expected x to be renamed to x'")
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
index 3ce96efd8f..0b544e080a 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
@@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.trex
 
 import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant}
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.lir.convenience.tla
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.tla
 
 /**
  * An abstract test suite that is parameterized by the snapshot type.
@@ -15,6 +15,10 @@ import at.forsyte.apalache.tla.lir.UntypedPredefs._
  *   the snapshot type
  */
 trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
+
+  def nX: TBuilderInstruction = tla.name("x", IntT1)
+  def nY: TBuilderInstruction = tla.name("y", IntT1)
+
   test("constant initialization") { exeCtx: ExecutorContextT =>
     // N' <- 1
     val trex = new TransitionExecutorImpl(Set("N"), Set("x", "y"), exeCtx)
@@ -22,7 +26,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     assert(trex.stepNo == 0)
     val constInit = mkAssign("N", 10)
     trex.initializeConstants(constInit)
-    val init = tla.and(mkAssign("x", tla.name("N")), mkAssign("y", 1))
+    val init = tla.and(mkAssignInt("x", tla.name("N", IntT1)), mkAssign("y", 1))
     // init is a potential transition with index 3 (the index is defined by the input spec)
     val isTranslated = trex.prepareTransition(3, init)
     assert(isTranslated)
@@ -32,7 +36,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     trex.nextState()
     assert(trex.stepNo == 1)
     // assert something about the current state
-    trex.assertState(tla.eql(tla.name("x"), tla.int(5)))
+    trex.assertState(tla.eql(nX, tla.int(5)))
     assert(trex.sat(60).contains(false))
   }
 
@@ -51,13 +55,13 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     trex.nextState()
     assert(trex.stepNo == 1)
     // assert something about the current state
-    trex.assertState(tla.eql(tla.name("y"), tla.int(1)))
+    trex.assertState(tla.eql(nY, tla.int(1)))
     assert(trex.sat(60).contains(true))
   }
 
   test("check enabled and discard") { exeCtx: ExecutorContextT =>
     // an obviously disabled transition: y' <- 1 /\ y' <- 2
-    val init = tla.and(mkAssign("y", 1), tla.eql(tla.prime(tla.name("y")), tla.int(2)), mkAssign("x", 3))
+    val init = tla.and(mkAssign("y", 1), tla.eql(tla.prime(nY), tla.int(2)), mkAssign("x", 3))
     val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
     trex.debug = true
     assert(trex.stepNo == 0)
@@ -83,7 +87,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // create a snapshot for a later rollback
     val snapshot = trex.snapshot()
     // assert invariant violation and check it
-    val notInv = tla.not(tla.eql(tla.prime(tla.name("y")), tla.prime(tla.name("x"))))
+    val notInv = tla.not(tla.eql(tla.prime(nY), tla.prime(nX)))
     trex.assertState(notInv)
     assert(trex.sat(60).contains(false))
     // rollback the snapshot
@@ -96,8 +100,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // x' <- 1 /\ y' <- 1
     val init: TlaEx = tla.and(mkAssign("y", 1), mkAssign("x", 1))
     // x' <- y /\ y' <- x + y
-    val trans1: TlaEx = tla.and(mkAssign("x", tla.name("y")), mkAssign("y", tla.plus(tla.name("x"), tla.name("y"))))
-    val trans2: TlaEx = tla.and(mkAssign("x", tla.name("x")), mkAssign("y", tla.name("y")))
+    val trans1: TlaEx =
+      tla.and(mkAssignInt("x", nY), mkAssignInt("y", tla.plus(nX, nY)))
+    val trans2: TlaEx = tla.and(mkAssignInt("x", nX), mkAssignInt("y", nY))
     val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
     trex.prepareTransition(1, init)
     trex.pickTransition()
@@ -123,17 +128,21 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     assert(Binding().toMap == decPath(0)._1)
     // state 1 is produced by transition 1
     assert(1 == decPath(1)._2)
-    assert(Map("x" -> tla.int(1).untyped(), "y" -> tla.int(1).untyped()) == decPath(1)._1)
+
+    def mapWithBuild(pairs: (String, TBuilderInstruction)*): Map[String, TlaEx] =
+      pairs.map { case (a, b) => a -> b.build }.toMap
+
+    assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(1)) == decPath(1)._1)
     // state 2 is produced by transition 1
     assert(1 == decPath(2)._2)
-    assert(Map("x" -> tla.int(1).untyped(), "y" -> tla.int(2).untyped()) == decPath(2)._1)
+    assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(2)) == decPath(2)._1)
     // state 3 is produced by transition 1
     assert(1 == decPath(3)._2)
-    assert(Map("x" -> tla.int(2).untyped(), "y" -> tla.int(3).untyped()) == decPath(3)._1)
+    assert(mapWithBuild("x" -> tla.int(2), "y" -> tla.int(3)) == decPath(3)._1)
     // state 4 is produced either by transition 1, or by transition 2
     assert(1 == decPath(4)._2 || 2 == decPath(4)._2)
-    assert(Map("x" -> tla.int(2).untyped(), "y" -> tla.int(3).untyped()) == decPath(4)._1
-      || Map("x" -> tla.int(3).untyped(), "y" -> tla.int(5).untyped()) == decPath(4)._1)
+    assert(mapWithBuild("x" -> tla.int(2), "y" -> tla.int(3)) == decPath(4)._1
+      || mapWithBuild("x" -> tla.int(3), "y" -> tla.int(5)) == decPath(4)._1)
 
     // test the symbolic execution
     val exe = trex.execution
@@ -143,23 +152,23 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
 
     // state 1 is the state right after Init, that is, Init(state0)
     val state1 = exe.path(1)._1
-    assertValid(trex, tla.eql(state1("x").toNameEx, tla.int(1)))
-    assertValid(trex, tla.eql(state1("y").toNameEx, tla.int(1)))
+    assertValid(trex, tla.eql(state1("x").toBuilder, tla.int(1)))
+    assertValid(trex, tla.eql(state1("y").toBuilder, tla.int(1)))
 
     // state 2 is the state Next(Init(state0))
     val state2 = exe.path(2)._1
-    assertValid(trex, tla.eql(state2("x").toNameEx, tla.int(1)))
-    assertValid(trex, tla.eql(state2("y").toNameEx, tla.int(2)))
+    assertValid(trex, tla.eql(state2("x").toBuilder, tla.int(1)))
+    assertValid(trex, tla.eql(state2("y").toBuilder, tla.int(2)))
 
     // state 3 is the state Next(Next(Init(state0)))
     val state3 = exe.path(3)._1
-    assertValid(trex, tla.eql(state3("x").toNameEx, tla.int(2)))
-    assertValid(trex, tla.eql(state3("y").toNameEx, tla.int(3)))
+    assertValid(trex, tla.eql(state3("x").toBuilder, tla.int(2)))
+    assertValid(trex, tla.eql(state3("y").toBuilder, tla.int(3)))
 
     // state 4 is the state Next(Next(Next(Init(state0)))
     val state4 = exe.path(4)._1
-    assertValid(trex, tla.or(tla.eql(state4("x").toNameEx, tla.int(2)), tla.eql(state4("x").toNameEx, tla.int(3))))
-    assertValid(trex, tla.or(tla.eql(state4("y").toNameEx, tla.int(3)), tla.eql(state4("y").toNameEx, tla.int(5))))
+    assertValid(trex, tla.or(tla.eql(state4("x").toBuilder, tla.int(2)), tla.eql(state4("x").toBuilder, tla.int(3))))
+    assertValid(trex, tla.or(tla.eql(state4("y").toBuilder, tla.int(3)), tla.eql(state4("y").toBuilder, tla.int(5))))
 
     // regression in multi-core
     val snapshot = trex.snapshot()
@@ -177,7 +186,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // x' <- 1 /\ y' <- 1
     val init = tla.and(mkAssign("y", 1), mkAssign("x", 1))
     // x' <- x /\ y' <- x + y
-    val nextTrans = tla.and(mkAssign("x", tla.name("x")), mkAssign("y", tla.plus(tla.name("x"), tla.name("y"))))
+    val nextTrans = tla.and(mkAssignInt("x", nX), mkAssignInt("y", tla.plus(nX, nY)))
     // push Init
     val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
     trex.prepareTransition(1, init)
@@ -186,10 +195,10 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // prepare Next
     trex.prepareTransition(1, nextTrans)
     // check what has changed
-    val inv0 = tla.ge(tla.name("x"), tla.int(3))
+    val inv0 = tla.ge(nX, tla.int(3))
     val mayChange0 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0)
     assert(!mayChange0)
-    val inv1 = tla.ge(tla.name("y"), tla.name("x"))
+    val inv1 = tla.ge(nY, nX)
     val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1)
     assert(mayChange1)
   }
@@ -198,7 +207,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     // y' <- 1
     val init = tla.and(mkAssign("y", 1))
     // y' <- y + 1
-    val nextTrans = mkAssign("y", tla.plus(tla.name("y"), tla.int(1)))
+    val nextTrans = mkAssignInt("y", tla.plus(nY, tla.int(1)))
     // push Init
     val trex = new TransitionExecutorImpl(Set.empty, Set("y"), exeCtx)
     trex.prepareTransition(1, init)
@@ -216,9 +225,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
     assert(!mayChange2)
   }
 
-  private def mkAssign(name: String, value: Int) =
-    tla.assignPrime(tla.name(name), tla.int(value))
+  private def mkAssign(name: String, value: Int): TBuilderInstruction =
+    tla.assign(tla.prime(tla.name(name, IntT1)), tla.int(value))
 
-  private def mkAssign(name: String, rhs: TlaEx) =
-    tla.assignPrime(tla.name(name), rhs)
+  private def mkAssignInt(name: String, rhs: TBuilderInstruction) =
+    tla.assign(tla.prime(tla.name(name, IntT1)), rhs)
 }