$  quint run ../examples/solidity/icse23-fig7/lottery.qnt 
module lottery {
  pure def MAX_UINT64 = ipow(2, 64)
  pure def MAX_UINT = ipow(2, 256)
  type Address = str
  type Uint64 = int
  val q::lastTrace = List()
  def q::test = ((q::nrunsArg_420, q::nstepsArg_420, q::initArg_420, q::nextArg_420, q::invArg_420) => false)
  action q::init = init
  action q::step = step
  val q::inv = true
  type Uint = int
  pure def getOrElse: ((a -> b), a, b) => b = ((m_114, key_114, default_114) => ite(in(key_114, keys(m_114)), get(m_114, key_114), default_114))
  type LotteryState = { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }
  val q::runResult = q::test(10000, 20, q::init, q::step, q::inv)
  pure def require: (bool, str) => str = ((cond_75, msg_75) => ite(cond_75, "", msg_75))
  pure def newLottery: (str) => { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str } = ((sender_129) => Rec("tickets", Map(), "winningId", 0, "drawingPhase", false, "owner", sender_129))
  type LotteryResult = (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str })
  pure def onlyOwner: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str) => str = ((state_63, addr_63) => ite(eq(addr_63, field(state_63, "owner")), "", "must be the owner"))
  pure def andRequire: (str, bool, str) => str = ((prevErr_93, cond_93, msg_93) => ite(neq(prevErr_93, ""), prevErr_93, require(cond_93, msg_93)))
  pure def returnError: (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((msg_38, state_38) => Tup(msg_38, state_38))
  pure def returnState: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_47) => Tup("", state_47))
  pure def reset: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_161, sender_161) => pure val err_159 = onlyOwner(state_161, sender_161) { ite(neq(err_159, ""), returnError(err_159, state_161), returnState(Rec("tickets", Map(), "winningId", 0, "drawingPhase", false, "owner", field(state_161, "owner")))) })
  pure def buy: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str, int, int) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_222, sender_222, id_222, amount_222) => pure val err_220 = andRequire(require(eq(field(state_222, "winningId"), 0), "already drawn"), not(field(state_222, "drawingPhase")), "drawing") { ite(neq(err_220, ""), returnError(err_220, state_222), pure val senderTickets_218 = getOrElse(field(state_222, "tickets"), sender_222, Map()) { pure val newAmounts_217 = put(senderTickets_218, id_222, getOrElse(senderTickets_218, id_222, amount_222)) { returnState(with(state_222, "tickets", put(field(state_222, "tickets"), sender_222, newAmounts_217))) } }) })
  pure def enterDrawingPhase: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_247, sender_247) => pure val err_245 = onlyOwner(state_247, sender_247) { ite(neq(err_245, ""), returnError(err_245, state_247), returnState(with(state_247, "drawingPhase", true))) })
  pure def draw: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str, int) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_288, sender_288, id_288) => pure val err_286 = andRequire(andRequire(require(eq(field(state_288, "winningId"), 0), "already drawn"), field(state_288, "drawingPhase"), "not drawing"), neq(id_288, 0), "invalid winning number") { ite(neq(err_286, ""), returnError(err_286, state_288), returnState(with(state_288, "winningId", id_288))) })
  action claimReward: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_314, sender_314) => pure val err_312 = require(neq(field(state_314, "winningId"), 0), "not drawn") { ite(neq(err_312, ""), returnError(err_312, state_314), returnState(state_314)) })
  action multiBuy: ({ tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }, str, List[int], List[int]) => (str, { tickets: (str -> (int -> int)), winningId: int, drawingPhase: bool, owner: str }) = ((state_410, sender_410, ids_410, amounts_410) => val err_408 = require(eq(field(state_410, "winningId"), 0), "already drawn") { ite(neq(err_408, ""), returnError(err_408, state_410), val senderTickets_406 = getOrElse(field(state_410, "tickets"), sender_410, Map()) { val newAmounts_405 = mapBy(union(keys(senderTickets_406), map(indices(ids_410), ((i_356) => nth(ids_410, i_356)))), ((id_392) => val topUp_391 = fold(map(filter(indices(ids_410), ((i_368) => eq(nth(ids_410, i_368), id_392))), ((i_374) => nth(amounts_410, i_374))), 0, ((sum_382, a_382) => iadd(sum_382, a_382))) { iadd(getOrElse(senderTickets_406, id_392, 0), topUp_391) })) { returnState(with(state_410, "tickets", put(field(state_410, "tickets"), sender_410, newAmounts_405))) } }) })
}
quint run <input>

Simulate a Quint specification and check invariants

Options:
  --help         Show help                                             [boolean]
  --version      Show version number                                   [boolean]
  --out          output file (suppresses all console output)            [string]
  --main         name of the main module (by default, computed from filename)
                                                                        [string]
  --out-itf      output the trace in the Informal Trace Format to file
                 (suppresses all console output)                        [string]
  --max-samples  the maximum on the number of traces to try
                                                       [number] [default: 10000]
  --max-steps    the maximum on the number of steps in every trace
                                                          [number] [default: 20]
  --init         name of the initializer action       [string] [default: "init"]
  --step         name of the step action              [string] [default: "step"]
  --invariant    invariant to check: a definition name or an expression
                                                    [string] [default: ["true"]]
  --seed         random seed to use for non-deterministic choice        [string]
  --verbosity    control how much output is produced (0 to 5)
                                                           [number] [default: 2]

Error: Internal error while flattening [QNT404] Name 'init' not found,[QNT404] Name 'step' not found
    at resolveNamesOrThrow (/quint/quint/dist/src/flattening/fullFlattener.js:91:15)
    at flattenModules (/quint/quint/dist/src/flattening/fullFlattener.js:62:35)
    at compileFromCode (/quint/quint/dist/src/runtime/compile.js:191:104)
    at compileAndRun (/quint/quint/dist/src/simulation.js:58:47)
    at runSimulator (/quint/quint/dist/src/cliCommands.js:392:51)
    at EitherConstructor.asyncChain (/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /quint/quint/dist/src/cli.js:33:39