diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
index ab0cda8aab..44ed32798e 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
@@ -54,7 +54,10 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
           case None =>
             // not found, just use the name
             // a value that was assigned by the solver, and not created by us
-            tla.str(cell.toString)
+            tt match {
+              case CellTFrom(StrT1)                => tla.str(s"FRESH${cell.id}")
+              case CellTFrom(ttConst @ ConstT1(_)) => tla.const(s"FRESH${cell.id}", ttConst)
+            }
         }
       }