# Reading from simple-session.transcript Verifying CheckWellformed$$_module.__default.A ... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [2 proof obligations] error transcript(3,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,13): Error: rbrace expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(6,2): Error: rbrace expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [0 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,0): Error: invalid VarDeclStatement Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(6,2): Error: EOF expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(6,2): Error: EOF expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [3 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(11,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(11,0): Error: semi expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(11,0): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,25): Error: openparen expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,25): Error: openparen expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,26): Error: invalid QSep Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,28): Error: invalid QSep Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,27): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [1 proof obligation] error transcript(10,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(12,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' transcript(24,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' transcript(24,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' transcript(24,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,14): Error: Duplicate member name: M' transcript(24,14): Error: Duplicate member name: M' transcript(33,14): Error: Duplicate member name: M' Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,14): Error: Duplicate member name: M transcript(33,14): Error: Duplicate member name: M Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [5 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... Retrieving cached verification result for implementation Impl$$_module.__default.M2... [5 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [2 proof obligations] error transcript(38,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(38,38): Error: semi expected Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [2 proof obligations] error transcript(38,9): Error: assertion violation Execution trace: (0,0): anon0 Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... Retrieving cached verification result for implementation Impl$$_module.__default.M2... [2 proof obligations] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,2): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,2): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,2): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,9): Error: invalid AssertStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,9): Error: invalid AssertStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(40,9): Error: unresolved identifier: fal Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(10,9): Warning: /!\ No terms found to trigger on. transcript(20,9): Warning: /!\ No terms found to trigger on. transcript(29,9): Warning: /!\ No terms found to trigger on. transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... [0 proof obligations] verified Verifying Impl$$_module.__default.A ... Retrieving cached verification result for implementation Impl$$_module.__default.A... [0 proof obligations] verified Verifying CheckWellformed$$_module.__default.M_k ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M_k... [0 proof obligations] verified Verifying Impl$$_module.__default.M_k ... Retrieving cached verification result for implementation Impl$$_module.__default.M_k... [1 proof obligation] verified Verifying CheckWellformed$$_module.__default.M0 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M0... [0 proof obligations] verified Verifying Impl$$_module.__default.M0 ... Retrieving cached verification result for implementation Impl$$_module.__default.M0... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M1 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M1... [0 proof obligations] verified Verifying Impl$$_module.__default.M1 ... Retrieving cached verification result for implementation Impl$$_module.__default.M1... [5 proof obligations] verified Verifying CheckWellformed$$_module.__default.M2 ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.M2... [0 proof obligations] verified Verifying Impl$$_module.__default.M2 ... Retrieving cached verification result for implementation Impl$$_module.__default.M2... [1 proof obligation] verified Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]]