Construct fresh model values

apalache-mc · Aug 16, 2023 · 75d6108 · 75d6108
1 parent b374361
commit 75d6108
Showing 1 changed file with 4 additions and 1 deletion.
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
@@ -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)
+            }
         }
       }