Fresh variable incorrectly chosen when using CHOOSE to select unique elements out of a set

## Description

A specification uses CHOOSE in top-level constants to get unique elements out of a set of uninterpreted types which successfully model checks with TLC results in a spurious invariant failure.
Using `Int` instead of an uninterpreted type results in a similar failure.

It appears that instead of choosing the second item in the set, a random fresh item is chosen instead, which appears to be a bug e.g. `{ "1_OF_ITEM", "FRESH29_OF_ITEM" }` instead of the expected `{ "1_OF_ITEM", "2_OF_ITEM" }`.

<img width="1003" height="446" alt="Image" src="https://github.com/user-attachments/assets/9ff0312d-dc8c-47a5-b9a9-6a6342535037" />

Related: #3149 

## Impact

No workaround found yet. High impact because it affects model checking correctness, and TLC exhibits correct behaviour here.

## Input specification

```
\* apalache-mc check --debug --cinit=ConstInit --inv=MyInvariant --temporal=TemporalInvariant LetBug.tla
\* [tla2tools.jar] -config LetBug.cfg -workers 6 LetBug.tla [-dump dot,actionlabels out.dot]

------------------------------- MODULE LetBug -------------------------------
\* Integers is required for `..` .
EXTENDS Integers, TLC

CONSTANT
  \* @type: Set(ITEM);
  Items

\* Used for TLC's constant assignment
\* Needed to make TLC run on this testcase for comparison.
ItemsDemo == 1..2

ConstInit ==
  /\ Items = {"1_OF_ITEM", "2_OF_ITEM"}

\* Deterministic version of Guess to avoid non-determinism
GuessDet(S) == CHOOSE x \in S: TRUE

\* Multi-step selection needed for cross-compatibility between TLC and Apalache.
\* It is a critical part of this testcase, and the proximate cause of the bug.
\* Apalache incorrectly generates "fresh values" not in the original set.
\* bucketItemsToAdd = { "1_OF_ITEM", "FRESH29_OF_ITEM" }
p1 == GuessDet(Items)
p2 == GuessDet(Items \ {p1})
\* @type: Set(ITEM);
BucketItems == {p1, p2}

\* Due to https://github.com/apalache-mc/apalache/issues/3149, the more concise Alternative doesn't work.
\* BucketItems == CHOOSE T \in SUBSET Items : Cardinality(T) = 2

VARIABLES
  \* @type: Set(ITEM);
  localBucket,
  \* @type: Set(ITEM);
  bucketItemsToAdd

\* Apalache needs this annotation.
\* @type: Seq(Set(ITEM));
vars == <<localBucket, bucketItemsToAdd>>

Init ==
  /\ localBucket = {}
  /\ bucketItemsToAdd = BucketItems

BucketAction == \E p \in bucketItemsToAdd:
/\ localBucket' = localBucket \union {p}
/\ bucketItemsToAdd' = bucketItemsToAdd \ {p}

\* Alternative deterministic LET-based variant (but with the same issue).
BucketActionLet == (bucketItemsToAdd /= {} /\
      LET p == GuessDet(bucketItemsToAdd) IN (
      /\ localBucket' = localBucket \union {p}
      /\ bucketItemsToAdd' = bucketItemsToAdd \ {p} )
     )

Next ==
\/ BucketAction
\/ UNCHANGED vars

MyInvariant ==
/\ localBucket \subseteq Items

Spec ==
/\ Init
/\ [][Next]_vars
\* Essential to avoid unwanted stuttering on BucketAction.
\* BucketAction should always happen.
/\ SF_bucketItemsToAdd(BucketAction)

TemporalInvariant == []<>(localBucket = BucketItems)

=============================================================================
```

## The command line parameters used to run the tool

`--debug --cinit=ConstInit --inv=MyInvariant --temporal=TemporalInvariant`

## Expected behavior

Successful model checking concurring with TLC behaviour.

## Log files

```
PASS #0: SanyParser                                               I@15:03:33.090
Parsing file [...]/LetBug.tla
Parsing file /tmp/SANYij04Fa5o9x/Integers.tla
Parsing file /tmp/SANYij04Fa5o9x/__rewire_tlc_in_apalache.tla
Parsing file /tmp/SANYij04Fa5o9x/Naturals.tla
PASS #1: TypeCheckerSnowcat                                       I@15:03:33.302
 > Running Snowcat .::.                                           I@15:03:33.302
 > Your types are purrfect!                                       I@15:03:33.653
 > All expressions are typed                                      I@15:03:33.653
PASS #2: ConfigurationPass                                        I@15:03:33.654
  > Set the initialization predicate to Init                      I@15:03:33.659
  > Set the transition predicate to Next                          I@15:03:33.659
  > Set the constant initialization predicate to ConstInit        I@15:03:33.660
  > Set an invariant to MyInvariant                               I@15:03:33.660
  > Set a temporal property to TemporalInvariant                  I@15:03:33.660
PASS #3: DesugarerPass                                            I@15:03:33.664
  > Desugaring...                                                 I@15:03:33.664
PASS #4: InlinePass                                               I@15:03:33.847
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, MyInvariant, Next, TemporalInvariant I@15:03:33.848
PASS #5: TemporalPass                                             I@15:03:33.878
  > Rewriting temporal operators...                               I@15:03:33.878
  > Found 1 temporal properties                                   I@15:03:33.883
  > Adding logic for loop finding                                 I@15:03:33.883
PASS #6: InlinePass                                               I@15:03:33.910
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, MyInvariant, Next, TemporalInvariant I@15:03:33.910
PASS #7: PrimingPass                                              I@15:03:33.917
  > Introducing ConstInitPrimed for ConstInit'                    I@15:03:33.919
  > Introducing InitPrimed for Init'                              I@15:03:33.924
PASS #8: VCGen                                                    I@15:03:33.925
  > Producing verification conditions from the invariant MyInvariant I@15:03:33.925
  > VCGen produced 1 verification condition(s)                    I@15:03:33.927
  > Producing verification conditions from the invariant TemporalInvariant I@15:03:33.930
  > VCGen produced 1 verification condition(s)                    I@15:03:33.930
PASS #9: PreprocessingPass                                        I@15:03:33.932
  > Before preprocessing: unique renaming                         I@15:03:33.932
 > Applying standard transformations:                             I@15:03:33.941
  > PrimePropagation                                              I@15:03:33.942
  > Desugarer                                                     I@15:03:33.944
  > UniqueRenamer                                                 I@15:03:33.947
  > Normalizer                                                    I@15:03:33.950
  > Keramelizer                                                   I@15:03:33.955
  > After preprocessing: UniqueRenamer                            I@15:03:33.962
No source location for expr@9512: ((∃p$1 ∈ bucketItemsToAdd: ((localBucket' = (localBucket ∪ {p$1})) ∧ ... E@15:03:33.982
No source location for expr@9535: (localBucket = {}) ∧ (bucketItemsToAdd = {CHOOSE x$7 ∈ Items : TRUE, ... E@15:03:33.983
No source location for expr@9582: (__InLoop ∧ (bucketItemsToAdd = __saved_bucketItemsToAdd) ∧ (localBuc... E@15:03:33.984
No source location for expr@9688: (localBucket' = {}) ∧ (bucketItemsToAdd' = {CHOOSE x$7 ∈ Items : TRUE... E@15:03:33.985
No source location for expr@9694: ¬(localBucket ⊆ Items)          E@15:03:33.986
No source location for expr@9582: (__InLoop ∧ (bucketItemsToAdd = __saved_bucketItemsToAdd) ∧ (localBuc... E@15:03:33.986
No source location for expr@9725: ¬((__InLoop ∧ (bucketItemsToAdd = __saved_bucketItemsToAdd) ∧ (localB... E@15:03:33.987
PASS #10: TransitionFinderPass                                    I@15:03:33.989
  > Found 1 initializing transitions                              I@15:03:34.014
  > Found 4 transitions                                           I@15:03:34.027
  > Found constant initializer ConstInit                          I@15:03:34.028
  > Applying unique renaming                                      I@15:03:34.031
PASS #11: OptimizationPass                                        I@15:03:34.044
 > Applying optimizations:                                        I@15:03:34.054
  > ConstSimplifier                                               I@15:03:34.055
  > ExprOptimizer                                                 I@15:03:34.068
  > SetMembershipSimplifier                                       I@15:03:34.076
  > ConstSimplifier                                               I@15:03:34.080
PASS #12: AnalysisPass                                            I@15:03:34.090
 > Marking skolemizable existentials and sets to be expanded...   I@15:03:34.095
  > Skolemization                                                 I@15:03:34.096
  > Expansion                                                     I@15:03:34.098
  > Remove unused let-in defs                                     I@15:03:34.102
 > Running analyzers...                                           I@15:03:34.107
  > Introduced expression grades                                  I@15:03:34.114
PASS #13: BoundedChecker                                          I@15:03:34.115
State 0: Checking 2 state invariants                              I@15:03:34.711
State 0: state invariant 0 holds.                                 I@15:03:34.714
State 0: state invariant 1 holds.                                 I@15:03:34.727
Step 0: picking a transition out of 1 transition(s)               I@15:03:34.728
State 1: Checking 2 state invariants                              I@15:03:34.827
Check the trace in: [...]/_apalache-out/LetBug.tla/2025-09-12T15-03-32_3547922445664835939/violation1.tla, [...]/_apalache-out/LetBug.tla/2025-09-12T15-03-32_3547922445664835939/MCviolation1.out, [...]/_apalache-out/LetBug.tla/2025-09-12T15-03-32_3547922445664835939/violation1.json, [...]/_apalache-out/LetBug.tla/2025-09-12T15-03-32_3547922445664835939/violation1.itf.json I@15:03:35.060
State 1: state invariant 0 violated.                              I@15:03:35.060
Found 1 error(s)                                                  I@15:03:35.061
Z3 statistics for context 0...                                    I@15:03:35.062
conflicts=2,decisions=34,propagations=245,final checks=3,added eqs=235,mk clause=208,del clause=1,num checks=5,mk bool var=227,arith-make-feasible=3,arith-max-columns=4,num allocs=77580,rlimit count=9584,max memory=17.62,memory=17.62
 I@15:03:35.064
The outcome is: Error                                             I@15:03:35.067
Checker has found an error                                        I@15:03:35.076
It took me 0 days  0 hours  0 min  2 sec                          I@15:03:35.076
Total time: 2.173 sec                                             I@15:03:35.077
EXITCODE: ERROR (12)
```

## System information

- Apalache version: `56462d3 build 56462d3` (revision `56462d384d63853ceb503c8eb86a4eff02572529` from `main` branch)
- OS: Ubuntu Linux x86_64 24.04
- JDK version: `21.0.3`

## Triage checklist (for maintainers)



- [ ] Reproduce the bug on the main development branch.
- [ ] Add the issue to the apalache GitHub project.
- [ ] If the bug is high impact, ensure someone available is assigned to fix it.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Uh oh!

Fresh variable incorrectly chosen when using CHOOSE to select unique elements out of a set #3165

Description

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Uh oh!

Fresh variable incorrectly chosen when using CHOOSE to select unique elements out of a set #3165

Description

Description

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions