Skip to content

Instantly share code, notes, and snippets.

@nishantjr

nishantjr/gist:4a9bd4570e07f5330d6f4ab67a2d6634

Created April 1, 2020 19:02
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save nishantjr/4a9bd4570e07f5330d6f4ab67a2d6634 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save nishantjr/4a9bd4570e07f5330d6f4ab67a2d6634 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
Kore version 0.0.1.0
Git:
revision: c2c9bca46d87a2e5237b40680cd667b5856ab3e2
branch: HEAD
last commit: 2020 Apr 1 13:21:24 -0500
Build date: 2020 Apr 02 00:31:47 +0530
[1/60] run: execution t/kool/dynamic-dispatch-1.dfy
FAILED: .build/t/kool/dynamic-dispatch-1.dfy.execution-run
./kdafny run --definition "execution" "t/kool/dynamic-dispatch-1.dfy" > ".build/t/kool/dynamic-dispatch-1.dfy.execution-run" || (cat .build/t/kool/dynamic-dispatch-1.dfy.execution-run ; false)
kore-exec: [2020-04-02 00:31:56.412331544] Error (ErrorException):
While applying axiom:
left:
/* Fn Sfc */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn Sfc */
Lbl'-LT-'T'-GT-'{}(
/* Fn Sfc */
Lbl'-LT-'threads'-GT-'{}(
/* Fn Sfc */
/* builtin: */
Lbl'Unds'ThreadCellMap'Unds'{}(
/* element: */ LblThreadCellMapItem{}(
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'k'-GT-'{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExp{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lbl'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa */
VarK0:SortExp{},
/* Fl Fn D Sfa */
VarHOLE:SortExps{}
)
),
/* Fl Fn D Sfa */ VarDotVar4:SortK{}
)
),
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{},
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{},
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{}
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar2:SortThreadCellMap{}
)
),
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{},
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{},
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{},
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{},
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{},
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{},
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{}
),
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
)
requires:
/* Spa */
\equals{SortBool{}, SortGeneratedTopCell{}}(
/* Fn Spa */
Lbl'Unds'andBool'Unds'{}(
/* Fl Fn D Spa */
Lbl'Unds'andBool'Unds'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"),
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true")
),
/* Fn Spa */
LblnotBool'Unds'{}(
/* Fn Spa */
LblisKResult{}(
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Spa */
/* Inj: */ inj{SortExps{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarHOLE:SortExps{}
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true")
)
existentials:
[]
right:
/* Fn Spa */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn Spa */
Lbl'-LT-'T'-GT-'{}(
/* Fn Spa */
Lbl'-LT-'threads'-GT-'{}(
/* Fn Spa */
/* builtin: */
Lbl'Unds'ThreadCellMap'Unds'{}(
/* element: */ LblThreadCellMapItem{}(
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{},
/* Fl Fn D Spa */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{},
/* Fl Fn D Spa */
Lbl'-LT-'k'-GT-'{}(
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Spa */
/* Inj: */ inj{SortExps{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarHOLE:SortExps{}
),
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Spa */
Lbl'Hash'freezer'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps0'Unds'{}(
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Spa */
/* Inj: */ inj{SortExp{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarK0:SortExp{}
),
/* Fl Fn D Sfa Cl */
dotk{}()
)
),
/* Fl Fn D Sfa */ VarDotVar4:SortK{}
)
)
),
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{},
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{},
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{}
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar2:SortThreadCellMap{}
)
),
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{},
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{},
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{},
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{},
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{},
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{},
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{}
),
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
)
ensures:
/* D Sfa */ \top{SortGeneratedTopCell{}}()
from the initial configuration:
\and{SortGeneratedTopCell{}}(
/* term: */
/* Fl Fn D Sfc */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fl Fn D Sfc */
Lbl'-LT-'T'-GT-'{}(
/* Fl Fn D Sfc */
Lbl'-LT-'threads'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
/* concrete element: */ LblThreadCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fl Fn D Sfc */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fl Fn D Sfc */
Lbl'-LT-'k'-GT-'{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExp{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa */
LbllookupMember'LParUndsCommUndsRParUnds'DAFNY'Unds'Exp'Unds'List'Unds'Id{}(
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */
Lbl'Stop'Map{}()
)
)
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cl */
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lblthis'Unds'DAFNY-SYNTAX'Unds'Exp{}()
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* Fl Fn D Sfc */
Lbl'-LT-'control'-GT-'{}(
/* Fl Fn D Sfc */
Lbl'-LT-'fstack'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
LblListItem{}(
/* Fl Fn D Sfc */
LblfstackFrame'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Map'Unds'K'Unds'List'Unds'Type'Unds'K{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}(),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cl */
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(),
/* Fl Fn D Sfa Cl */ dotk{}()
),
/* Fl Fn D Sfa */
/* builtin: */ Lbl'Stop'List{}(),
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortCrntObjCell{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object")
),
/* Fl Fn D Sfa */
Lbl'-LT-'envStack'-GT-'{}(
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Stop'List{}()
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'LocationCell{}()
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'xstack'-GT-'{}(
/* Fl Fn D Sfa */
/* builtin: */ Lbl'Stop'List{}()
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'returnType'-GT-'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa */
Lbl'-LT-'envStack'-GT-'{}(
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */
Lbl'Stop'Map{}()
)
)
)
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'LocationCell{}()
)
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'env'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'holds'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
)
)
)
),
/* Fl Fn D Sfc */
Lbl'-LT-'store'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVal{}, SortKItem{}}(
/* Fl Fn D Sfa */
LblobjectClosure'LParUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Id'Unds'List{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"),
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
)
)
)
)
)
),
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("1")
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVal{}, SortKItem{}}(
/* Fl Fn D Sfc */
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}(
/* Fl Fn D Sfa Cl */
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}()
),
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}()
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortBlock{}, SortStmt{}}(
/* Fl Fn D Sfc */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortVal{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}("\x0a")
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'busy'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}()
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'terminated'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}()
),
/* Fl Fn D Sfa */
Lbl'-LT-'input'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
),
/* Fl Fn D Sfa */
Lbl'-LT-'output'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'nextLoc'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2")
),
/* Fl Fn D Sfc */
Lbl'-LT-'classes'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
Lbl'Unds'ClassDataCellMap'Unds'{}(
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmts{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}()
)
),
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
Lbl'Unds'ClassDataCellMap'Unds'{}(
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmts{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("2")
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfc */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object")
),
/* Fl Fn D Sfc */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortKItem{}}(
/* Fl Fn D Sfc */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfc */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortVal{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}("\x0a")
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
)
))
)
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
),
\and{SortGeneratedTopCell{}}(
/* predicate: */
/* D Sfa */ \top{SortGeneratedTopCell{}}(),
/* substitution: */
\top{SortGeneratedTopCell{}}()
))
with the unifier:
\and{_PREDICATE{}}(
/* term: */
/* D Sfa */ \top{_PREDICATE{}}(),
\and{_PREDICATE{}}(
/* predicate: */
\and{_PREDICATE{}}(
/* Sfc */
\ceil{SortBool{}, _PREDICATE{}}(
/* Fn Sfc */
LblisKResult{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExps{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarHOLE:SortExps{}
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
),
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fn Sfc */
LblnotBool'Unds'{}(
/* Fn Sfc */
LblisKResult{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExps{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarHOLE:SortExps{}
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
),
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true")
),
/* Sfa */
\equals{SortExp{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa */
LbllookupMember'LParUndsCommUndsRParUnds'DAFNY'Unds'Exp'Unds'List'Unds'Id{}(
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
)
)
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsLSqBUndsRSqBUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa */ VarK0:SortExp{},
/* Fl Fn D Sfa */ VarHOLE:SortExps{}
)
)
)),
/* substitution: */
\and{_PREDICATE{}}(
/* Spa */
\equals{SortIdCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'0:SortIdCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
),
\and{_PREDICATE{}}(
/* Spc */
\equals{SortControlCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'1:SortControlCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'control'-GT-'{}(
/* Fl Fn D Sfc */
Lbl'-LT-'fstack'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
LblListItem{}(
/* Fl Fn D Sfc */
LblfstackFrame'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Map'Unds'K'Unds'List'Unds'Type'Unds'K{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}(),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cl */
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(),
/* Fl Fn D Sfa Cl */ dotk{}()
),
/* Fl Fn D Sfa */
/* builtin: */ Lbl'Stop'List{}(),
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortCrntObjCell{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object")
),
/* Fl Fn D Sfa */
Lbl'-LT-'envStack'-GT-'{}(
/* Fl Fn D Sfa */
/* builtin: */ Lbl'Stop'List{}()
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'LocationCell{}()
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'xstack'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'returnType'-GT-'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfa */
Lbl'-LT-'envStack'-GT-'{}(
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
)
)
)
),
/* Fl Fn D Sfa Cl */ Lbl'Stop'LocationCell{}()
)
)
),
\and{_PREDICATE{}}(
/* Spc */
\equals{SortClassesCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'10:SortClassesCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'classes'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
Lbl'Unds'ClassDataCellMap'Unds'{}(
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmts{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}()
)
),
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
Lbl'Unds'ClassDataCellMap'Unds'{}(
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C2")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "C1")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmts{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraRBraUnds'DAFNY-SYNTAX'Unds'Block{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblint'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfa Cl */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("2")
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* concrete element: */ LblClassDataCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfc */
Lbl'-LT-'classData'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'className'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'baseClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Object")
),
/* Fl Fn D Sfc */
Lbl'-LT-'declarations'-GT-'{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortKItem{}}(
/* Fl Fn D Sfc */
Lbl'UndsUndsLParUndsRParUndsUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Id'Unds'Params'Unds'Block{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfc */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortVal{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}("\x0a")
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
)
))
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortEnvCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'2:SortEnvCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'env'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortHoldsCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'3:SortHoldsCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'holds'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}()
)
),
\and{_PREDICATE{}}(
/* Spc */
\equals{SortStoreCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'4:SortStoreCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'store'-GT-'{}(
/* Fl Fn D Sfc */
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVal{}, SortKItem{}}(
/* Fl Fn D Sfa */
LblobjectClosure'LParUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Id'Unds'List{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"),
/* Fl Fn D Sfa */
/* builtin: */
Lbl'Unds'List'Unds'{}(
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Main")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortInt{}}("1")
)
)
)
),
LblListItem{}(
/* Fl Fn D Sfa Cl */
LblenvStackFrame'LParUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Id'Unds'Map{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"Object"),
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
)
)
)
)
)
),
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("1")
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVal{}, SortKItem{}}(
/* Fl Fn D Sfc */
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}(
/* Fl Fn D Sfa Cl */
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types{}(
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}(),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Types'Unds'Type'Unds'Types'QuotRBraUnds'Types{}()
),
/* Fl Fn D Sfa Cl */
Lblvoid'Unds'DAFNY-SYNTAX'Unds'Type{}()
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main"),
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0"),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Params'Unds'Param'Unds'Params'QuotRBraUnds'Params{}(),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortBlock{}, SortStmt{}}(
/* Fl Fn D Sfc */
Lbl'LBraUndsRBraUnds'DAFNY-SYNTAX'Unds'Block'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C1"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortDecl{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lbl'UndsUndsSClnUnds'DAFNY-SYNTAX'Unds'Decl'Unds'Type'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsEqlsUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
Lblnew'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Id'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"C2"),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa */
Lblprint'LParUndsRParSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exps{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o1")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m1")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}(" ")
),
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfa Cl */
Lbl'UndsStopUndsUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Id{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortExp{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"o2")
),
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */
"m2")
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa Cl */
Lbl'UndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortString{}, SortVal{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */
\dv{SortString{}}("\x0a")
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortBusyCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'5:SortBusyCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'busy'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortTerminatedCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'6:SortTerminatedCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'terminated'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Set{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortInputCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'7:SortInputCell{},
/* Fl Fn D Sfa */
Lbl'-LT-'input'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortOutputCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'8:SortOutputCell{},
/* Fl Fn D Sfa */
Lbl'-LT-'output'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortNextLocCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'9:SortNextLocCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'nextLoc'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2")
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortGeneratedCounterCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortThreadCellMap{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar2:SortThreadCellMap{},
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'ThreadCellMap{}()
),
/* Spa */
\equals{SortK{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar4:SortK{},
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cl */
Lbl'Hash'freezer'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp0'Unds'{}(),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'UndsSClnUnds'DAFNY-SYNTAX'Unds'Stmt'Unds'Exp{}(
/* Fl Fn D Sfa Cl */
Lblthis'Unds'DAFNY-SYNTAX'Unds'Exp{}()
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
)))))))))))))
))
Failed substitution coverage check!
The substitution (above, in the unifier) did not cover the axiom variables:
VarHOLE:SortExps{} VarK0:SortExp{}
in the left-hand side of the axiom.
CallStack (from HasCallStack):
error, called at src/Kore/Step/Step.hs:394:6 in kore-0.0.1.0-CDi4oyRprcp5AMiB47zztY:Kore.Step.Step
[Error] Critical: Haskell Backend execution failed with code 1 and produced no
output.
ninja: build stopped: subcommand failed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment