Skip to content

Instantly share code, notes, and snippets.

@nishantjr

nishantjr/gist:f2a69058a6635173645e41bcdd175895

Created April 1, 2020 17:39
Show Gist options
  • Save nishantjr/f2a69058a6635173645e41bcdd175895 to your computer and use it in GitHub Desktop.
Save nishantjr/f2a69058a6635173645e41bcdd175895 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
[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-01 23:06:57.513474233] 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'5:SortIdCell{},
/* Fl Fn D Sfc */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa */ Var'Unds'5: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 Sfc */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVal{}, SortExp{}}(
/* Fl Fn D Sfa */
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}(
/* Fl Fn D Sfa */
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}(
/* Fl Fn D Sfa */
Var'Unds'0:SortTypes{},
/* Fl Fn D Sfa */
VarT:SortType{}
),
/* Fl Fn D Sfa */
VarClass:SortId{},
/* Fl Fn D Sfa */
VarOL:SortInt{},
/* Fl Fn D Sfa */
VarPs:SortParams{},
/* Fl Fn D Sfa */
VarS:SortStmt{}
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortVals{}, SortExps{}}(
/* Fl Fn D Sfa */
VarVs:SortVals{}
)
)
),
/* Fl Fn D Sfa */ VarK:SortK{}
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'control'-GT-'{}(
/* Fl Fn D Sfa */
Lbl'-LT-'fstack'-GT-'{}(
/* Fl Fn D Sfa */ VarDotVar5:SortList{}
),
/* Fl Fn D Sfa */
Lbl'-LT-'xstack'-GT-'{}(
/* Fl Fn D Sfa */ VarXS:SortList{}
),
/* Fl Fn D Sfa */
Lbl'-LT-'returnType'-GT-'{}(
/* Fl Fn D Sfa */ VarT'Apos':SortType{}
),
/* Fl Fn D Sfa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa */
Var'Unds'2:SortCrntClassCell{},
/* Fl Fn D Sfa */
Var'Unds'3:SortEnvStackCell{},
/* Fl Fn D Sfa */
Var'Unds'4:SortLocationCell{}
)
),
/* Fl Fn D Sfa */
Lbl'-LT-'env'-GT-'{}(
/* Fl Fn D Sfa */ VarEnv:SortMap{}
),
/* Fl Fn D Sfa */ Var'Unds'6:SortHoldsCell{}
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar3:SortThreadCellMap{}
)
),
/* Fn Sfc */
Lbl'-LT-'store'-GT-'{}(
/* Fn Sfc */
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarOL:SortInt{}
),
/* 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 */ Var'Unds'1:SortId{},
/* Fl Fn D Sfa */ VarEStack:SortList{}
)
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar2:SortMap{}
)
),
/* Fl Fn D Sfa */ Var'Unds'7:SortBusyCell{},
/* Fl Fn D Sfa */ Var'Unds'8:SortTerminatedCell{},
/* Fl Fn D Sfa */ Var'Unds'9:SortInputCell{},
/* Fl Fn D Sfa */ Var'Unds'10:SortOutputCell{},
/* Fl Fn D Sfa */ Var'Unds'11:SortNextLocCell{},
/* Fl Fn D Sfa */ Var'Unds'12:SortClassesCell{}
),
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
)
requires:
/* D Sfa */ \top{SortGeneratedTopCell{}}()
existentials:
[]
right:
/* Fn */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn */
Lbl'-LT-'T'-GT-'{}(
/* Fn */
Lbl'-LT-'threads'-GT-'{}(
/* Fn */
/* builtin: */
Lbl'Unds'ThreadCellMap'Unds'{}(
/* element: */ LblThreadCellMapItem{}(
/* Fl Fn D Sfa */ Var'Unds'5:SortIdCell{},
/* Fn */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa */ Var'Unds'5:SortIdCell{},
/* Fn Spa */
Lbl'-LT-'k'-GT-'{}(
/* Fn Spa */
kseq{}(
/* Fn Spa */
/* Inj: */ inj{SortStmts{}, SortKItem{}}(
/* Fn Spa */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fn Spa */
LblmkDecls'LParUndsCommUndsRParUnds'DAFNY'Unds'Stmts'Unds'Params'Unds'Vals{}(
/* Fl Fn D Sfa */
VarPs:SortParams{},
/* Fl Fn D Sfa */
VarVs:SortVals{}
),
/* Fl Fn D Spa */
Lbl'UndsUndsUnds'DAFNY-SYNTAX'Unds'Stmts'Unds'Stmts'Unds'Stmts{}(
/* Fl Fn D Spa */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa */
VarS:SortStmt{}
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortStmt{}, SortStmts{}}(
/* Fl Fn D Sfa Cl */
Lblreturn'SClnUnds'DAFNY-SYNTAX'Unds'Stmt{}()
)
)
)
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
),
/* Fl Fn D Spa */
Lbl'-LT-'control'-GT-'{}(
/* Fl Fn D Spa */
Lbl'-LT-'fstack'-GT-'{}(
/* Fl Fn D Spa */
Lbl'Unds'List'Unds'{}(
/* Fl Fn D Spa */
/* builtin: */
LblListItem{}(
/* Fl Fn D Spa */
LblfstackFrame'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'KItem'Unds'Map'Unds'K'Unds'List'Unds'Type'Unds'K{}(
/* Fl Fn D Sfa */
VarEnv:SortMap{},
/* Fl Fn D Sfa */
VarK:SortK{},
/* Fl Fn D Sfa */
VarXS:SortList{},
/* Fl Fn D Sfa */
VarT'Apos':SortType{},
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Spa */
/* Inj: */ inj{SortCrntObjCell{}, SortKItem{}}(
/* Fl Fn D Spa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Sfa */
Var'Unds'2:SortCrntClassCell{},
/* Fl Fn D Sfa */
Var'Unds'3:SortEnvStackCell{},
/* Fl Fn D Sfa */
Var'Unds'4:SortLocationCell{}
)
),
/* Fl Fn D Sfa Cl */
dotk{}()
)
)
),
/* Fl Fn D Sfa */
VarDotVar5:SortList{}
)
),
/* Fl Fn D Spa */
Lbl'-LT-'xstack'-GT-'{}(
/* Fl Fn D Sfa */ VarXS:SortList{}
),
/* Fl Fn D Spa */
Lbl'-LT-'returnType'-GT-'{}(
/* Fl Fn D Sfa */ VarT:SortType{}
),
/* Fl Fn D Spa */
Lbl'-LT-'crntObj'-GT-'{}(
/* Fl Fn D Spa */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa */ VarClass:SortId{}
),
/* Fl Fn D Spa */
Lbl'-LT-'envStack'-GT-'{}(
/* Fl Fn D Sfa */
VarEStack:SortList{}
),
/* Fl Fn D Sfa Cl */
Lbl'Stop'LocationCell{}()
)
),
/* Fl Fn D */
Lbl'-LT-'env'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ Lbl'Stop'Map{}()
),
/* Fl Fn D Sfa */ Var'Unds'6:SortHoldsCell{}
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar3:SortThreadCellMap{}
)
),
/* Fn Sfc */
Lbl'-LT-'store'-GT-'{}(
/* Fn Sfc */
/* builtin: */
Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa */ VarOL:SortInt{}
),
/* 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 */ Var'Unds'1:SortId{},
/* Fl Fn D Sfa */ VarEStack:SortList{}
)
)
),
/* opaque child: */ /* Fl Fn D Sfa */
VarDotVar2:SortMap{}
)
),
/* Fl Fn D Sfa */ Var'Unds'7:SortBusyCell{},
/* Fl Fn D Sfa */ Var'Unds'8:SortTerminatedCell{},
/* Fl Fn D Sfa */ Var'Unds'9:SortInputCell{},
/* Fl Fn D Sfa */ Var'Unds'10:SortOutputCell{},
/* Fl Fn D Sfa */ Var'Unds'11:SortNextLocCell{},
/* Fl Fn D Sfa */ Var'Unds'12:SortClassesCell{}
),
/* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
)
ensures:
/* D Sfa */ \top{SortGeneratedTopCell{}}()
from the initial configuration:
\and{SortGeneratedTopCell{}}(
/* term: */
/* Fn Sfc */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn Sfc */
Lbl'-LT-'T'-GT-'{}(
/* Fn Sfc */
Lbl'-LT-'threads'-GT-'{}(
/* Fn Sfc */
/* builtin: */
/* concrete element: */ LblThreadCellMapItem{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fn Sfc */
Lbl'-LT-'thread'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("0")
),
/* Fn Sfc */
Lbl'-LT-'k'-GT-'{}(
/* Fn Sfc */
kseq{}(
/* Fn Sfc */
/* Inj: */ inj{SortExp{}, SortKItem{}}(
/* Fn Sfa */
Lbl'UndsLParUndsRParUnds'DAFNY-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exps{}(
/* Fn 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{}}(
/* Sfa */
\ceil{SortExp{}, _PREDICATE{}}(
/* Fn 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")
)
),
/* Sfc */
\equals{SortExp{}, _PREDICATE{}}(
/* Fn 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 Sfc */
/* Inj: */ inj{SortVal{}, SortExp{}}(
/* Fl Fn D Sfa */
LblmethodClosure'LParUndsCommUndsCommUndsCommUndsCommUndsRParUnds'DAFNY'Unds'Val'Unds'Type'Unds'Id'Unds'Int'Unds'Params'Unds'Stmt{}(
/* Fl Fn D Sfa */
Lbl'Unds'-'-GT-UndsUnds'DAFNY-SYNTAX'Unds'Type'Unds'Types'Unds'Type{}(
/* Fl Fn D Sfa */ Var'Unds'0:SortTypes{},
/* Fl Fn D Sfa */ VarT:SortType{}
),
/* Fl Fn D Sfa */ VarClass:SortId{},
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0"),
/* Fl Fn D Sfa */ VarPs:SortParams{},
/* Fl Fn D Sfa */ VarS:SortStmt{}
)
)
)
),
/* substitution: */
\and{_PREDICATE{}}(
/* Spa */
\equals{SortId{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'1:SortId{},
/* Fl Fn D Sfa Cl */ \dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortOutputCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'10: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'11:SortNextLocCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'nextLoc'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2")
)
),
\and{_PREDICATE{}}(
/* Spc */
\equals{SortClassesCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'12: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{SortCrntClassCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'2:SortCrntClassCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'crntClass'-GT-'{}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortEnvStackCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'3:SortEnvStackCell{},
/* 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{}()
)
)
)
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortLocationCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'4:SortLocationCell{},
/* Fl Fn D Sfa Cl */ Lbl'Stop'LocationCell{}()
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortIdCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'5:SortIdCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'id'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortHoldsCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'6:SortHoldsCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'holds'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}()
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortBusyCell{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ Var'Unds'7: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'8: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'9:SortInputCell{},
/* Fl Fn D Sfa */
Lbl'-LT-'input'-GT-'{}(
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
)
),
\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{}}(
/* Spc */
\equals{SortMap{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar2:SortMap{},
/* Fl Fn D Sfc */
/* builtin: */
/* 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{SortThreadCellMap{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar3:SortThreadCellMap{},
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'ThreadCellMap{}()
),
\and{_PREDICATE{}}(
/* Spc */
\equals{SortList{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarDotVar5:SortList{},
/* 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{}()
)
)
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortList{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarEStack:SortList{},
/* 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{}()
)
)
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortMap{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarEnv:SortMap{},
/* Fl Fn D Sfa Cl */ /* builtin: */ Lbl'Stop'Map{}()
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortK{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarK: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{}()
)
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortInt{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarOL:SortInt{},
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortType{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarT'Apos':SortType{},
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortType{}}(
/* Fl Fn D Sfa Cl */
\dv{SortId{}}(/* Fl Fn D Sfa Cl */ "Main")
)
),
\and{_PREDICATE{}}(
/* Spa */
\equals{SortVals{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarVs:SortVals{},
/* Fl Fn D Sfa Cl */
Lbl'Stop'List'LBraQuotUndsCommUndsUnds'DAFNY-SYNTAX'Unds'Vals'Unds'Val'Unds'Vals'QuotRBraUnds'Vals{}()
),
/* Spa */
\equals{SortList{}, _PREDICATE{}}(
/* Fl Fn D Sfa */ VarXS:SortList{},
/* Fl Fn D Sfa */ /* builtin: */ Lbl'Stop'List{}()
)
))))))))))))))))))))))
))
Failed substitution coverage check!
The substitution (above, in the unifier) did not cover the axiom variables:
Var'Unds'0:SortTypes{}
VarClass:SortId{}
VarPs:SortParams{}
VarS:SortStmt{}
VarT:SortType{}
in the left-hand side of the axiom.
CallStack (from HasCallStack):
error, called at src/Kore/Step/Step.hs:393: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