;;; -*- scheme -*-
;;; Anonymized phenom MicroIonGaugeImpl (anon2.dzn from anon_phenom/),
;;; renamed `_5` → `anon_phenom_micro_ion` so the runner's `-m $name`
;;; finds it. Captures the phenom 15-fail bug.
;;;
;;; Numbers (env-on / env-off / golden):
;;;   step_frontier:  14544 states  (env-on)
;;;   DAG:            14968 states  (env-off)
;;;   dzn golden:     26212 states  (`dzn verify --out=aut`)
;;;
;;; Both engines fail weak-failures equivalence vs golden in BOTH
;;; directions (fwd=false, bwd=false). The bug is in shared
;;; infrastructure used by both engines, NOT a step_frontier
;;; regression.
;;;
;;; Investigation notes (commit 193317f0 + follow-up):
;;;
;;; 1. Counter-example trace from `ltscompare -c` (after stripping
;;;    `<state>` labels): `_56._225 → _110._226 → _110.return →
;;;    _104._225 → _104.return → _109._228 → _109._169:_151`. Both
;;;    LTSes have this trace, but their refusal sets at the end
;;;    differ.
;;;
;;; 2. Label-set diff: golden has `_56._305:_147`, `_101._59:_147`,
;;;    several `port.<state>(_59:value)` labels we don't. Stripping
;;;    `<state>` labels from both still fails the comparison.
;;;
;;; 3. Root pattern: the missing reply value `_56._305:_147` requires
;;;    the comp_var `_92` to reach `_145._147`, which only happens
;;;    along a deep dependency chain:
;;;      a. handler in `[_64._77]` block reaches via `_56._78`
;;;         (advances `_64` from initial `_111` to `_77` via
;;;         `_189(_59._77)` in another branch);
;;;      b. that handler calls local fn `_191(_176)`;
;;;      c. `_191` calls `_102._186 → _193 → _194` chain;
;;;      d. `_102._194()` returning `_169._196` triggers
;;;         `_92 = _145._147`;
;;;      e. handler then `_189(_59._117)` advances `_64`;
;;;      f. later `_56._303` event runs, `_301()` returns
;;;         `_24._59._147`, and the handler replies with
;;;         `_305._147`.
;;;
;;; 4. We DO reach `_64 == _77` (some handler advances it correctly).
;;;    We DO call `_102._194()` and see all 3 outcomes (`_146`/
;;;    `_151`/`_195`/`_196`). But somewhere the chain breaks — our
;;;    LTS has zero occurrences of `_147` in any reply value.
;;;
;;; 5. Both DAG and step_frontier produce nearly-identical (14544 vs
;;;    14968) wrong output. The shared code path is `eval_func_lts`
;;;    in `exec.rs` (called when a local fn appears in expression
;;;    context like `_24._59 _304 = _301();`) and/or interface state
;;;    advance after multi-clause iface event replies.
;;;
;;; 6. Golden's `aut-failures` (7344 states) and `aut-weak-trace`
;;;    (7050 states) minimized formats also don't match — confirms
;;;    the bug isn't a label-convention mismatch.
;;;
;;; The handler bodies that matter for the missing path are at
;;; lines 333 (`_56._225` in `[_64._111]`), 446 (`_56._78` in
;;; `[_64._77]`), 183 (`_191`), 1017 (`_301`). Reading these and
;;; manually executing the state machine should pinpoint exactly
;;; which transition our engine drops.

((skip-wfc) (queue-size-external 2))
