Skip to content

Commit

Permalink
Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratif…
Browse files Browse the repository at this point in the history
…iedRules/aux/caches/UninterpretedLiteralCache.scala

Co-authored-by: Thomas Pani <[email protected]>
  • Loading branch information
Kukovec and thpani authored Aug 10, 2023
1 parent c1a0d6d commit a9935a9
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.{ConstT1, StrT1, TlaType1}
import at.forsyte.apalache.tla.types.tla

/**
* A cache for uninterpreted literals, that are translated as uninterpreted SMT constants, with a unique sort per
* A cache for uninterpreted literals, that are translated to uninterpreted SMT constants, with a unique sort per
* uninterpreted type. Since two values are equal iff they are literally the same literal, we force inequality between
* all the respective SMT constants.
*
Expand Down

0 comments on commit a9935a9

Please sign in to comment.