From 80ee397a6fba3381441bf709a40923683d995e92 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 24 Aug 2023 16:28:49 +0200 Subject: [PATCH] Explanation of caseAssertions behavior (#2707) --- .../at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala index f72c3aa1c9..8762c1f364 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala @@ -49,8 +49,12 @@ trait Oracle extends Serializable { assertions: Seq[TBuilderInstruction], elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { size match { + // If the oracle has no candidate values, then caseAssertions should return a no-op for SMT, i.e. TRUE. case 0 => state.arena.cellTrue().toBuilder + // If the oracle has a single candidate value, then the chosen value will always equal to the (sole) candidate value. + // In other words, for such an oracle, whenEqualTo(..., 0) will always hold. + // Therefore, we don't need an ITE (and don't need to consider elseAssertions), we just take the first assertion. case 1 => assertions.head case _ =>