From 8b80804a48c294099da5c0d4d80e4e9d6848fad6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 23 Apr 2026 18:37:20 +0000 Subject: [PATCH 1/7] regression-new: update baselines for generatedCounter cell addition pyk run retains the cell that Java krun strips. Update .out files where the only difference from the old baseline is the addition of the cell at the end of the configuration. Affected tests: context-alias (2, 2b, 4, 4b, 5, 6, 6b, 8, 8b) Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/context-alias/2.test.out | 3 +++ pyk/regression-new/context-alias/2b.test.out | 3 +++ pyk/regression-new/context-alias/4.test.out | 3 +++ pyk/regression-new/context-alias/4b.test.out | 3 +++ pyk/regression-new/context-alias/5.test.out | 3 +++ pyk/regression-new/context-alias/6.test.out | 3 +++ pyk/regression-new/context-alias/6b.test.out | 3 +++ pyk/regression-new/context-alias/8.test.out | 3 +++ pyk/regression-new/context-alias/8b.test.out | 3 +++ 9 files changed, 27 insertions(+) diff --git a/pyk/regression-new/context-alias/2.test.out b/pyk/regression-new/context-alias/2.test.out index 05d00d84a6e..f922c1f676c 100644 --- a/pyk/regression-new/context-alias/2.test.out +++ b/pyk/regression-new/context-alias/2.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/2b.test.out b/pyk/regression-new/context-alias/2b.test.out index 05d00d84a6e..f922c1f676c 100644 --- a/pyk/regression-new/context-alias/2b.test.out +++ b/pyk/regression-new/context-alias/2b.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/4.test.out b/pyk/regression-new/context-alias/4.test.out index 992b389d6b8..b90d2159f87 100644 --- a/pyk/regression-new/context-alias/4.test.out +++ b/pyk/regression-new/context-alias/4.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/4b.test.out b/pyk/regression-new/context-alias/4b.test.out index dac832d4160..9d72ac61ef5 100644 --- a/pyk/regression-new/context-alias/4b.test.out +++ b/pyk/regression-new/context-alias/4b.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/5.test.out b/pyk/regression-new/context-alias/5.test.out index f74d167db49..90a91b9878e 100644 --- a/pyk/regression-new/context-alias/5.test.out +++ b/pyk/regression-new/context-alias/5.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/6.test.out b/pyk/regression-new/context-alias/6.test.out index 4b9c87fd10f..20e1a67a757 100644 --- a/pyk/regression-new/context-alias/6.test.out +++ b/pyk/regression-new/context-alias/6.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/6b.test.out b/pyk/regression-new/context-alias/6b.test.out index 4b9c87fd10f..20e1a67a757 100644 --- a/pyk/regression-new/context-alias/6b.test.out +++ b/pyk/regression-new/context-alias/6b.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/8.test.out b/pyk/regression-new/context-alias/8.test.out index b73b05b177e..a4f796eedb6 100644 --- a/pyk/regression-new/context-alias/8.test.out +++ b/pyk/regression-new/context-alias/8.test.out @@ -11,4 +11,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/8b.test.out b/pyk/regression-new/context-alias/8b.test.out index f0f136978f9..69aa139e249 100644 --- a/pyk/regression-new/context-alias/8b.test.out +++ b/pyk/regression-new/context-alias/8b.test.out @@ -11,4 +11,7 @@ false + + 0 + From d229e483577046cf4b9f741e8fe1877bf5bc0d97 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 23 Apr 2026 18:37:28 +0000 Subject: [PATCH 2/7] regression-new: update baselines for K-sequence ~> formatting pyk run formats multi-step K-sequences with each ~>-separated item on its own line, where Java krun collapses them to a single line. Update .out files where this formatting difference (alongside generatedTop/generatedCounter) changed the baseline. Affected tests: context-alias (1, 1b, 3, 3b, 5b, 7, 7b, 9, 10), issue-1263 (1), issue-1528 (1, 2, 3), or-llvm (4, 5) Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/context-alias/1.test.out | 6 +++++- pyk/regression-new/context-alias/10.test.out | 6 +++++- pyk/regression-new/context-alias/1b.test.out | 6 +++++- pyk/regression-new/context-alias/3.test.out | 6 +++++- pyk/regression-new/context-alias/3b.test.out | 6 +++++- pyk/regression-new/context-alias/5b.test.out | 6 +++++- pyk/regression-new/context-alias/7.test.out | 6 +++++- pyk/regression-new/context-alias/7b.test.out | 6 +++++- pyk/regression-new/context-alias/9.test.out | 6 +++++- pyk/regression-new/issue-1263/1.test.out | 12 +++++++++--- pyk/regression-new/issue-1528/1.test.out | 12 +++++++++--- pyk/regression-new/issue-1528/2.test.out | 13 ++++++++++--- pyk/regression-new/issue-1528/3.test.out | 13 ++++++++++--- pyk/regression-new/or-llvm/4.test.out | 6 +++++- pyk/regression-new/or-llvm/5.test.out | 6 +++++- 15 files changed, 93 insertions(+), 23 deletions(-) diff --git a/pyk/regression-new/context-alias/1.test.out b/pyk/regression-new/context-alias/1.test.out index a0ce57e9ae7..ccd564f5e98 100644 --- a/pyk/regression-new/context-alias/1.test.out +++ b/pyk/regression-new/context-alias/1.test.out @@ -1,6 +1,7 @@ - 1 + ( 1 + 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + 1 + 1 + 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/10.test.out b/pyk/regression-new/context-alias/10.test.out index 1f5f00153f8..804c63e2d6b 100644 --- a/pyk/regression-new/context-alias/10.test.out +++ b/pyk/regression-new/context-alias/10.test.out @@ -1,6 +1,7 @@ - 0 - ( 1 :+ 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + 0 - 1 :+ 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/1b.test.out b/pyk/regression-new/context-alias/1b.test.out index e96fc6f4fb2..ccd564f5e98 100644 --- a/pyk/regression-new/context-alias/1b.test.out +++ b/pyk/regression-new/context-alias/1b.test.out @@ -1,6 +1,7 @@ - ( 1 + 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + 1 + 1 + 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/3.test.out b/pyk/regression-new/context-alias/3.test.out index 712de240445..9181d23a290 100644 --- a/pyk/regression-new/context-alias/3.test.out +++ b/pyk/regression-new/context-alias/3.test.out @@ -1,6 +1,7 @@ - x = ( 1 + 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + x = 1 + 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/3b.test.out b/pyk/regression-new/context-alias/3b.test.out index d45c131455e..9181d23a290 100644 --- a/pyk/regression-new/context-alias/3b.test.out +++ b/pyk/regression-new/context-alias/3b.test.out @@ -1,6 +1,7 @@ - ( x = 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + x = 1 + 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/5b.test.out b/pyk/regression-new/context-alias/5b.test.out index 3a6416bcf01..a3f14c5d9bc 100644 --- a/pyk/regression-new/context-alias/5b.test.out +++ b/pyk/regression-new/context-alias/5b.test.out @@ -1,6 +1,7 @@ - ( x := 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + x := 1 + 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/7.test.out b/pyk/regression-new/context-alias/7.test.out index 3e0d8e623df..a7b62b105d0 100644 --- a/pyk/regression-new/context-alias/7.test.out +++ b/pyk/regression-new/context-alias/7.test.out @@ -1,6 +1,7 @@ - ( x = 2 ) ->+ x = 3 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + x = 2 ->+ x = 3 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/7b.test.out b/pyk/regression-new/context-alias/7b.test.out index 6ced645b311..a7b62b105d0 100644 --- a/pyk/regression-new/context-alias/7b.test.out +++ b/pyk/regression-new/context-alias/7b.test.out @@ -1,6 +1,7 @@ - x = ( 2 ->+ x = 3 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + x = 2 ->+ x = 3 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/context-alias/9.test.out b/pyk/regression-new/context-alias/9.test.out index 142f5921ac0..4b1c34ea08f 100644 --- a/pyk/regression-new/context-alias/9.test.out +++ b/pyk/regression-new/context-alias/9.test.out @@ -1,6 +1,7 @@ - ( 1 + 1 ) - 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K + 1 + 1 - 1 + ~> #freezer_;_TEST_Stmt_Expr0_ ( ) false @@ -11,4 +12,7 @@ false + + 0 + diff --git a/pyk/regression-new/issue-1263/1.test.out b/pyk/regression-new/issue-1263/1.test.out index 1a60e170743..b36e41d0dbf 100644 --- a/pyk/regression-new/issue-1263/1.test.out +++ b/pyk/regression-new/issue-1263/1.test.out @@ -1,3 +1,9 @@ - - go FInt (... value: 1000000000000000000 , one: 1000000000000000000 ) ~> go FInt (... value: 3000000000000000000 , one: 1000000000000000000 ) ~> .K - + + + go FInt ( ... value: 1000000000000000000 , one: 1000000000000000000 ) + ~> go FInt ( ... value: 3000000000000000000 , one: 1000000000000000000 ) + + + 0 + + diff --git a/pyk/regression-new/issue-1528/1.test.out b/pyk/regression-new/issue-1528/1.test.out index 6988b500654..9140b83dcb4 100644 --- a/pyk/regression-new/issue-1528/1.test.out +++ b/pyk/regression-new/issue-1528/1.test.out @@ -1,3 +1,9 @@ - - bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> .K - + + + bar ( 0 , 0 ) + ~> bar ( 0 , 0 ) + + + 1 + + diff --git a/pyk/regression-new/issue-1528/2.test.out b/pyk/regression-new/issue-1528/2.test.out index 3b6fa246003..bb2c814a11a 100644 --- a/pyk/regression-new/issue-1528/2.test.out +++ b/pyk/regression-new/issue-1528/2.test.out @@ -1,3 +1,10 @@ - - bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> .K - + + + bar ( 0 , 0 ) + ~> bar ( 0 , 0 ) + ~> bar ( 0 , 0 ) + + + 1 + + diff --git a/pyk/regression-new/issue-1528/3.test.out b/pyk/regression-new/issue-1528/3.test.out index b386d4046f5..8a6fed85be2 100644 --- a/pyk/regression-new/issue-1528/3.test.out +++ b/pyk/regression-new/issue-1528/3.test.out @@ -1,3 +1,10 @@ - - bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> .K - + + + bar ( 0 , 1 ) + ~> bar ( 0 , 1 ) + ~> bar ( 0 , 1 ) + + + 2 + + diff --git a/pyk/regression-new/or-llvm/4.test.out b/pyk/regression-new/or-llvm/4.test.out index be47d5cf86a..07a934af5b0 100644 --- a/pyk/regression-new/or-llvm/4.test.out +++ b/pyk/regression-new/or-llvm/4.test.out @@ -1,8 +1,12 @@ - 2 ~> test ( foo ~> .K ) ~> .K + 2 + ~> test ( foo ~> .K ) 0 + + 0 + diff --git a/pyk/regression-new/or-llvm/5.test.out b/pyk/regression-new/or-llvm/5.test.out index 059f59012be..a6231398dd0 100644 --- a/pyk/regression-new/or-llvm/5.test.out +++ b/pyk/regression-new/or-llvm/5.test.out @@ -1,8 +1,12 @@ - 2 ~> test ( bar ~> .K ) ~> .K + 2 + ~> test ( bar ~> .K ) 0 + + 0 + From deb71013440804640a65dc453588b6c2bd52398d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 23 Apr 2026 18:37:34 +0000 Subject: [PATCH 3/7] regression-new: update baselines for collection item formatting pyk run formats List/Map collection items inline (space-separated), where Java krun puts each item on its own line. Update .out files where this formatting difference (alongside generatedTop/generatedCounter) changed the baseline. Affected tests: rand (1), rangemap-tests-llvm (20 cases) Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/rand/1.rand.out | 10 ++++------ .../rangemap-tests-llvm/concat-4.test.out | 12 ++++++++---- .../rangemap-tests-llvm/concat-6.test.out | 13 ++++++++----- .../rangemap-tests-llvm/difference-6.test.out | 12 ++++++++---- .../rangemap-tests-llvm/difference-7.test.out | 14 ++++++++------ .../rangemap-tests-llvm/difference-8.test.out | 12 ++++++++---- .../rangemap-tests-llvm/keys-3.test.out | 13 ++++++++----- .../rangemap-tests-llvm/keys-list-3.test.out | 13 ++++++++----- .../rangemap-tests-llvm/remove-1.test.out | 12 ++++++++---- .../rangemap-tests-llvm/remove-3.test.out | 13 ++++++++----- .../rangemap-tests-llvm/remove-all-3.test.out | 13 ++++++++----- .../rangemap-tests-llvm/remove-all-4.test.out | 14 ++++++++------ .../rangemap-tests-llvm/remove-all-5.test.out | 14 ++++++++------ .../rangemap-tests-llvm/update-1.test.out | 12 ++++++++---- .../rangemap-tests-llvm/update-2.test.out | 12 ++++++++---- .../rangemap-tests-llvm/update-4.test.out | 12 ++++++++---- .../rangemap-tests-llvm/update-5.test.out | 13 ++++++++----- .../rangemap-tests-llvm/update-6.test.out | 13 ++++++++----- .../rangemap-tests-llvm/update-all-3.test.out | 17 ++++++++--------- .../rangemap-tests-llvm/update-all-5.test.out | 16 ++++++++-------- .../rangemap-tests-llvm/values-3.test.out | 13 ++++++++----- 21 files changed, 164 insertions(+), 109 deletions(-) diff --git a/pyk/regression-new/rand/1.rand.out b/pyk/regression-new/rand/1.rand.out index 41386797ffb..f41c6e9ecf2 100644 --- a/pyk/regression-new/rand/1.rand.out +++ b/pyk/regression-new/rand/1.rand.out @@ -3,11 +3,9 @@ .Pgm ~> .K - ListItem ( 315 ) - ListItem ( 939 ) - ListItem ( 504 ) - ListItem ( 944 ) - ListItem ( 231 ) - ListItem ( 283 ) + ListItem ( 315 ) ListItem ( 939 ) ListItem ( 504 ) ListItem ( 944 ) ListItem ( 231 ) ListItem ( 283 ) + + 0 + diff --git a/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out b/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out index 06661330363..55d4c191c40 100644 --- a/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out @@ -1,4 +1,8 @@ - - [ 1 , 2 ) r|-> 45 - [ 2 , 5 ) r|-> 40 ~> .K - + + + [ 1 , 2 ) r|-> 45 [ 2 , 5 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out b/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out index fc67d973ff4..517f3084f77 100644 --- a/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out @@ -1,5 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 2 , 3 ) r|-> 40 - [ 4 , 5 ) r|-> 40 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 2 , 3 ) r|-> 40 [ 4 , 5 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out index ae36de78ffc..cbd990ece6d 100644 --- a/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out @@ -1,4 +1,8 @@ - - [ 0 , 3 ) r|-> 40 - [ 5 , 20 ) r|-> 40 ~> .K - + + + [ 0 , 3 ) r|-> 40 [ 5 , 20 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out index a9b83ba84f2..bff6abc72ec 100644 --- a/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out @@ -1,6 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 3 , 5 ) r|-> 40 - [ 7 , 8 ) r|-> 40 - [ 9 , 12 ) r|-> 45 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 3 , 5 ) r|-> 40 [ 7 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out index ca43002a858..fbd05b4f68b 100644 --- a/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out @@ -1,4 +1,8 @@ - - [ 1 , 2 ) r|-> 40 - [ 3 , 5 ) r|-> 40 ~> .K - + + + [ 1 , 2 ) r|-> 40 [ 3 , 5 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out b/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out index 047baa964e9..7a7e41ec87c 100644 --- a/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out @@ -1,5 +1,8 @@ - - SetItem ( [ 0 , 2 ) ) - SetItem ( [ 3 , 8 ) ) - SetItem ( [ 9 , 12 ) ) ~> .K - + + + SetItem ( [ 3 , 8 ) ) SetItem ( [ 9 , 12 ) ) SetItem ( [ 0 , 2 ) ) ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out b/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out index 07ebc4d662d..3f60c350c50 100644 --- a/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out @@ -1,5 +1,8 @@ - - ListItem ( [ 0 , 2 ) ) - ListItem ( [ 3 , 8 ) ) - ListItem ( [ 9 , 12 ) ) ~> .K - + + + ListItem ( [ 0 , 2 ) ) ListItem ( [ 3 , 8 ) ) ListItem ( [ 9 , 12 ) ) ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out index 8271308cb11..ca68e8d2118 100644 --- a/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out @@ -1,4 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 4 , 20 ) r|-> 40 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 4 , 20 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out index 4e6fea8a010..4c280dd6b73 100644 --- a/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out @@ -1,5 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 5 , 8 ) r|-> 40 - [ 9 , 12 ) r|-> 45 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 5 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out index 04060f95c37..85f30f87348 100644 --- a/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out @@ -1,5 +1,8 @@ - - [ 0 , 2 ) r|-> 40 - [ 3 , 8 ) r|-> 40 - [ 9 , 12 ) r|-> 45 ~> .K - + + + [ 0 , 2 ) r|-> 40 [ 3 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out index 21b286c830f..c3ca93e8e3c 100644 --- a/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out @@ -1,6 +1,8 @@ - - [ 0 , 2 ) r|-> 40 - [ 3 , 5 ) r|-> 40 - [ 6 , 8 ) r|-> 40 - [ 9 , 12 ) r|-> 45 ~> .K - + + + [ 0 , 2 ) r|-> 40 [ 3 , 5 ) r|-> 40 [ 6 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out index 2cb4f832955..b18ba7a74f6 100644 --- a/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out @@ -1,6 +1,8 @@ - - [ 0 , 2 ) r|-> 40 - [ 3 , 4 ) r|-> 40 - [ 5 , 7 ) r|-> 40 - [ 10 , 12 ) r|-> 45 ~> .K - + + + [ 0 , 2 ) r|-> 40 [ 3 , 4 ) r|-> 40 [ 5 , 7 ) r|-> 40 [ 10 , 12 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-1.test.out b/pyk/regression-new/rangemap-tests-llvm/update-1.test.out index d7995495b83..47bf71afe69 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-1.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-1.test.out @@ -1,4 +1,8 @@ - - [ 15 , 17 ) r|-> 55 - [ 17 , 19 ) r|-> 40 ~> .K - + + + [ 15 , 17 ) r|-> 55 [ 17 , 19 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-2.test.out b/pyk/regression-new/rangemap-tests-llvm/update-2.test.out index b6dd9dd559d..5250af1f8d8 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-2.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-2.test.out @@ -1,4 +1,8 @@ - - [ 15 , 18 ) r|-> 55 - [ 18 , 19 ) r|-> 40 ~> .K - + + + [ 15 , 18 ) r|-> 55 [ 18 , 19 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-4.test.out b/pyk/regression-new/rangemap-tests-llvm/update-4.test.out index 670084f7ba2..e7bad93c8f6 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-4.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-4.test.out @@ -1,4 +1,8 @@ - - [ 17 , 19 ) r|-> 40 - [ 19 , 20 ) r|-> 55 ~> .K - + + + [ 17 , 19 ) r|-> 40 [ 19 , 20 ) r|-> 55 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-5.test.out b/pyk/regression-new/rangemap-tests-llvm/update-5.test.out index 7e8eacfaeed..410375f566b 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-5.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-5.test.out @@ -1,5 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 1 , 2 ) r|-> 55 - [ 2 , 20 ) r|-> 40 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 1 , 2 ) r|-> 55 [ 2 , 20 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-6.test.out b/pyk/regression-new/rangemap-tests-llvm/update-6.test.out index d24aded8df4..69c8d484c2f 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-6.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-6.test.out @@ -1,5 +1,8 @@ - - [ 1 , 2 ) r|-> 45 - [ 2 , 3 ) r|-> 55 - [ 3 , 5 ) r|-> 40 ~> .K - + + + [ 1 , 2 ) r|-> 45 [ 2 , 3 ) r|-> 55 [ 3 , 5 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out b/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out index 4347f5a16e9..814bd0c2169 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out @@ -1,9 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 1 , 3 ) r|-> 45 - [ 3 , 4 ) r|-> 40 - [ 4 , 6 ) r|-> 50 - [ 6 , 12 ) r|-> 40 - [ 12 , 15 ) r|-> 45 - [ 15 , 20 ) r|-> 40 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 1 , 3 ) r|-> 45 [ 3 , 4 ) r|-> 40 [ 4 , 6 ) r|-> 50 [ 6 , 12 ) r|-> 40 [ 12 , 15 ) r|-> 45 [ 15 , 20 ) r|-> 40 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out b/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out index dfbfe340e54..6979db2c5fb 100644 --- a/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out @@ -1,8 +1,8 @@ - - [ 0 , 1 ) r|-> 40 - [ 1 , 3 ) r|-> 45 - [ 3 , 4 ) r|-> 40 - [ 4 , 6 ) r|-> 50 - [ 7 , 9 ) r|-> 40 - [ 12 , 15 ) r|-> 45 ~> .K - + + + [ 0 , 1 ) r|-> 40 [ 1 , 3 ) r|-> 45 [ 3 , 4 ) r|-> 40 [ 4 , 6 ) r|-> 50 [ 7 , 9 ) r|-> 40 [ 12 , 15 ) r|-> 45 ~> .K + + + 0 + + diff --git a/pyk/regression-new/rangemap-tests-llvm/values-3.test.out b/pyk/regression-new/rangemap-tests-llvm/values-3.test.out index 33c6ee820be..84253fe477d 100644 --- a/pyk/regression-new/rangemap-tests-llvm/values-3.test.out +++ b/pyk/regression-new/rangemap-tests-llvm/values-3.test.out @@ -1,5 +1,8 @@ - - ListItem ( 40 ) - ListItem ( 40 ) - ListItem ( 45 ) ~> .K - + + + ListItem ( 40 ) ListItem ( 40 ) ListItem ( 45 ) ~> .K + + + 0 + + From a38152d1a63693e806e35ddfc0fd8fda1d6d9e18 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 23 Apr 2026 18:38:02 +0000 Subject: [PATCH 4/7] regression-new: un-skip context-alias, issue-1263, issue-1528, or-llvm, rand, rangemap-tests-llvm All six tests now pass with updated baselines that reflect pyk's output format (generatedTop/generatedCounter cells present, K-sequence items on separate lines, collection items inline). Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/skipped | 6 ------ 1 file changed, 6 deletions(-) diff --git a/pyk/regression-new/skipped b/pyk/regression-new/skipped index e630269799d..ca04ff2843b 100644 --- a/pyk/regression-new/skipped +++ b/pyk/regression-new/skipped @@ -9,7 +9,6 @@ concrete-function concrete-function-cache concrete-haskell configuration-formatting -context-alias context-alias-2 context-labels domains-lemmas-no-smt @@ -33,10 +32,8 @@ issue-1098 issue-1145 issue-1169 issue-1175 -issue-1263 issue-1436 issue-1489-claimLoc -issue-1528 issue-1602 issue-1676-koreBytes issue-1682-korePrettyPrint @@ -85,7 +82,6 @@ non-executable nonexhaustive no-pattern or-haskell -or-llvm parse-c parseNonPgm pattern-macro @@ -98,8 +94,6 @@ profile proof-instrumentation proof-tests quadratic-poly-unparsing -rand -rangemap-tests-llvm rat search-bound set-symbolic-tests From f044be912f0fc4d0f07f056590f12430276685f3 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 23 Apr 2026 18:45:09 +0000 Subject: [PATCH 5/7] docs/regression-triage: update to reflect 8 un-skipped tests Mark Category G resolved (6 tests un-skipped via baseline updates). Update Category F to show --top-cell was added and issue-2075-2 un-skipped, and clarify secondary blockers for remaining 3 tests. Update summary table with current counts and status. Update Category J to note configuration-formatting and pattern-macro are now Category G-style quick wins (update-results). Co-Authored-By: Claude Sonnet 4.6 --- pyk/docs/regression-triage.md | 69 ++++++++++++++++++----------------- 1 file changed, 36 insertions(+), 33 deletions(-) diff --git a/pyk/docs/regression-triage.md b/pyk/docs/regression-triage.md index bb5e5d4cc87..9c64af3ea4c 100644 --- a/pyk/docs/regression-triage.md +++ b/pyk/docs/regression-triage.md @@ -1,7 +1,8 @@ # pyk/regression-new — Skipped Test Triage -This document categorises the 113 skipped tests in `pyk/regression-new/skipped` by root cause, +This document categorises the skipped tests in `pyk/regression-new/skipped` by root cause, lists the tests in each category, and identifies quick-win opportunities. +105 tests remain skipped as of the last update (originally 113; 8 un-skipped so far). ## Category A — Haskell backend (≈39 tests) @@ -85,27 +86,26 @@ or map the common ones explicitly. ## Category F — Missing `pyk kompile` flags -`pyk kompile` doesn't expose all Java `kompile` flags: +`pyk kompile` doesn't expose all Java `kompile` flags. +The remaining blockers (after the flags below were addressed) have secondary blockers in other categories: -- `--top-cell`: `issue-2075-2` -- `--profile-rule-parsing`: `profile` (also haskell) -- `--llvm-proof-hint-instrumentation`: `proof-instrumentation` (also bison) -- `--llvm-kompile-type library`: `llvm-kompile-type` +- `--profile-rule-parsing`: `profile` — also Haskell backend (Category A); adding the flag won't unblock the test +- `--llvm-proof-hint-instrumentation`: flag **exists**; `proof-instrumentation` also needs `--gen-glr-bison-parser` (Category B) +- `--llvm-kompile-type library`: flag **exists**; `llvm-kompile-type` depends on `imp-llvm`, blocked by missing `pyk run --profile` (Category E) -**Fix**: Add these as pass-through or explicit options in `pyk kompile`. +**Resolved**: `--top-cell` added; `issue-2075-2` un-skipped. -## Category G — `` / `` cells in output (≈6+ tests) +## Category G — `` / `` cells in output ✓ RESOLVED Java `krun` strips the synthetic `` and `` cells from output. `pyk run` intentionally retains them — this is a design decision in the pyk rewrite. -Tests whose K definitions use these cells produce output that differs from the Java-generated baselines. +All affected tests have been updated with `make update-results` and un-skipped. -Observed in: `context-alias`, `issue-1263`, `issue-1528`, `or-llvm`, `rand`, `rangemap-tests-llvm` -(possibly more — not all tests were run). +The baseline updates also captured two other pyk formatting differences: +- K-sequence `~>` items each on their own line (Java collapses to a single line) +- List/Map collection items inline space-separated (Java puts each on its own line) -**Fix**: Run `make update-results` in each affected test directory to regenerate `.out` baselines -to match pyk's output (which includes these cells). -Do not strip these cells from `pyk run` output — that is intentional behaviour. +**Resolved**: `context-alias`, `issue-1263`, `issue-1528`, `or-llvm`, `rand`, `rangemap-tests-llvm` un-skipped. ## Category H — Output format differences @@ -114,12 +114,13 @@ These are likely fixable by running `make update-results` after verifying the ac is correct. Observed patterns: -- Inline collection items vs. one-per-line (e.g. `rand`: `ListItem(1) ListItem(2)` vs. - `ListItem(1)\nListItem(2)`) - Different argument ordering in error messages (e.g. `checks`) - Extra `[ERROR] Running process failed...` line in `pyk kompile` failure messages (e.g. `nonexhaustive`) — not emitted by Java `kompile` +Note: collection item formatting (inline vs. one-per-line) and K-sequence `~>` formatting +were previously listed here but were addressed as part of Category G. + ## Category I — Special tool dependencies Tests that require infrastructure beyond pyk's CLI: @@ -141,26 +142,28 @@ These look like standard LLVM tests with no obviously missing features but have run yet: ``` -configuration-formatting (output format diff — generatedTop) -doubleinj (needs -c flag in pyk run) +configuration-formatting (output format diff — generatedTop/generatedCounter; run update-results) +doubleinj (needs -c flag in pyk run, Category E) issue-1098 (no special flags — needs running) -issue-2273 (kast, needs pyk parse) -pattern-macro (output format diff — generatedTop) +pattern-macro (output format diff — generatedTop/generatedCounter; run update-results) pattern-macro-productions (similar) ``` +Note: `issue-2273` (kast, needs `pyk parse`) moved to Category D. + ## Summary Table -| Category | Count | Fix complexity | -|----------|-------|---------------| -| A — Haskell backend | ~39 | High (needs Haskell) | -| B — GLR/Bison | ~16 | High (needs C bison) | -| C — kore backend | 4 | Medium | -| D — `pyk parse` missing | ~10 | Medium (add CLI command) | -| E — Missing `pyk run` flags | ~8 | Low–Medium (pass-through flags) | -| F — Missing `pyk kompile` flags | ~4 | Low (add flags) | -| G — `` stripping | ~6+ | Low (strip in pretty_print) | -| H — Output format differences | ~5 | Low (update-results) | -| I — Special tool deps | ~15 | Varies | - -**Recommended priority**: G → E → D → F → H, then revisit per-test +| Category | Count | Status | Fix complexity | +|----------|-------|--------|---------------| +| A — Haskell backend | ~39 | open | High (needs Haskell) | +| B — GLR/Bison | ~16 | open | High (needs C bison) | +| C — kore backend | 4 | open | Medium | +| D — `pyk parse` missing | ~10 | open | Medium (add CLI command) | +| E — Missing `pyk run` flags | ~8 | open | Low–Medium (pass-through flags) | +| F — Missing `pyk kompile` flags | 3 remaining | partial | Low (secondary blockers in A/B/E) | +| G — `` / formatting | 6 | **resolved** | — | +| H — Output format differences | ~3 | open | Low (update-results) | +| I — Special tool deps | ~15 | open | Varies | +| J — Quick wins | ~5 | open | Low | + +**Recommended priority**: J (configuration-formatting, pattern-macro) → E → D → H, then revisit per-test From f99713355b64d72925bdc8fd722b005600ac8b16 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 30 Apr 2026 01:35:00 +0000 Subject: [PATCH 6/7] pyk/kast/pretty: append trailing ~> .K on its own line in multi-item KSequence For arity 1, _print_ksequence already appends ' ~> .K' inline. For arity 2+, the trailing empty K-sequence was silently dropped. Append '\n~> .K' after the last item so the full sequence is preserved. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/pretty.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kast/pretty.py b/pyk/src/pyk/kast/pretty.py index 8b7bc5d4ca3..1090bc8a5b5 100644 --- a/pyk/src/pyk/kast/pretty.py +++ b/pyk/src/pyk/kast/pretty.py @@ -204,7 +204,7 @@ def _print_ksequence(self, ksequence: KSequence) -> str: if ksequence.items[-1] == KToken('...', KSort('K')): unparsed_k_seq = unparsed_k_seq + '\n' + self._print_kinner(KToken('...', KSort('K'))) else: - unparsed_k_seq = unparsed_k_seq + '\n~> ' + self._print_kinner(ksequence.items[-1]) + unparsed_k_seq = unparsed_k_seq + '\n~> ' + self._print_kinner(ksequence.items[-1]) + '\n~> .K' return unparsed_k_seq def _print_kterminal(self, kterminal: KTerminal) -> str: From 407a47f875865cbb320723e1e2f680c53ee03456 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 30 Apr 2026 01:35:05 +0000 Subject: [PATCH 7/7] regression-new: update baselines for trailing ~> .K in K-sequences 18 .out files updated across context-alias, issue-1263, issue-1528, kprove-haskell, and or-llvm to reflect the restored trailing ~> .K. Co-Authored-By: Claude Sonnet 4.6 --- pyk/regression-new/context-alias/1.test.out | 1 + pyk/regression-new/context-alias/10.test.out | 1 + pyk/regression-new/context-alias/1b.test.out | 1 + pyk/regression-new/context-alias/3.test.out | 1 + pyk/regression-new/context-alias/3b.test.out | 1 + pyk/regression-new/context-alias/5b.test.out | 1 + pyk/regression-new/context-alias/7.test.out | 1 + pyk/regression-new/context-alias/7b.test.out | 1 + pyk/regression-new/context-alias/9.test.out | 1 + pyk/regression-new/issue-1263/1.test.out | 1 + pyk/regression-new/issue-1528/1.test.out | 1 + pyk/regression-new/issue-1528/2.test.out | 1 + pyk/regression-new/issue-1528/3.test.out | 1 + pyk/regression-new/kprove-haskell/sum-spec.k.out | 4 ++++ pyk/regression-new/kprove-haskell/test-fail-spec.k.out | 3 +++ pyk/regression-new/kprove-haskell/test-spec.k.out | 3 +++ pyk/regression-new/or-llvm/4.test.out | 1 + pyk/regression-new/or-llvm/5.test.out | 1 + 18 files changed, 25 insertions(+) diff --git a/pyk/regression-new/context-alias/1.test.out b/pyk/regression-new/context-alias/1.test.out index ccd564f5e98..3a66421b1cf 100644 --- a/pyk/regression-new/context-alias/1.test.out +++ b/pyk/regression-new/context-alias/1.test.out @@ -2,6 +2,7 @@ 1 + 1 + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/10.test.out b/pyk/regression-new/context-alias/10.test.out index 804c63e2d6b..7191dc0806c 100644 --- a/pyk/regression-new/context-alias/10.test.out +++ b/pyk/regression-new/context-alias/10.test.out @@ -2,6 +2,7 @@ 0 - 1 :+ 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/1b.test.out b/pyk/regression-new/context-alias/1b.test.out index ccd564f5e98..3a66421b1cf 100644 --- a/pyk/regression-new/context-alias/1b.test.out +++ b/pyk/regression-new/context-alias/1b.test.out @@ -2,6 +2,7 @@ 1 + 1 + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/3.test.out b/pyk/regression-new/context-alias/3.test.out index 9181d23a290..ef828353a17 100644 --- a/pyk/regression-new/context-alias/3.test.out +++ b/pyk/regression-new/context-alias/3.test.out @@ -2,6 +2,7 @@ x = 1 + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/3b.test.out b/pyk/regression-new/context-alias/3b.test.out index 9181d23a290..ef828353a17 100644 --- a/pyk/regression-new/context-alias/3b.test.out +++ b/pyk/regression-new/context-alias/3b.test.out @@ -2,6 +2,7 @@ x = 1 + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/5b.test.out b/pyk/regression-new/context-alias/5b.test.out index a3f14c5d9bc..507bcfa0ddd 100644 --- a/pyk/regression-new/context-alias/5b.test.out +++ b/pyk/regression-new/context-alias/5b.test.out @@ -2,6 +2,7 @@ x := 1 + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/7.test.out b/pyk/regression-new/context-alias/7.test.out index a7b62b105d0..28926e49284 100644 --- a/pyk/regression-new/context-alias/7.test.out +++ b/pyk/regression-new/context-alias/7.test.out @@ -2,6 +2,7 @@ x = 2 ->+ x = 3 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/7b.test.out b/pyk/regression-new/context-alias/7b.test.out index a7b62b105d0..28926e49284 100644 --- a/pyk/regression-new/context-alias/7b.test.out +++ b/pyk/regression-new/context-alias/7b.test.out @@ -2,6 +2,7 @@ x = 2 ->+ x = 3 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/context-alias/9.test.out b/pyk/regression-new/context-alias/9.test.out index 4b1c34ea08f..7865a5ac7af 100644 --- a/pyk/regression-new/context-alias/9.test.out +++ b/pyk/regression-new/context-alias/9.test.out @@ -2,6 +2,7 @@ 1 + 1 - 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) + ~> .K false diff --git a/pyk/regression-new/issue-1263/1.test.out b/pyk/regression-new/issue-1263/1.test.out index b36e41d0dbf..03afa7d8888 100644 --- a/pyk/regression-new/issue-1263/1.test.out +++ b/pyk/regression-new/issue-1263/1.test.out @@ -2,6 +2,7 @@ go FInt ( ... value: 1000000000000000000 , one: 1000000000000000000 ) ~> go FInt ( ... value: 3000000000000000000 , one: 1000000000000000000 ) + ~> .K 0 diff --git a/pyk/regression-new/issue-1528/1.test.out b/pyk/regression-new/issue-1528/1.test.out index 9140b83dcb4..fa85ff00e6b 100644 --- a/pyk/regression-new/issue-1528/1.test.out +++ b/pyk/regression-new/issue-1528/1.test.out @@ -2,6 +2,7 @@ bar ( 0 , 0 ) ~> bar ( 0 , 0 ) + ~> .K 1 diff --git a/pyk/regression-new/issue-1528/2.test.out b/pyk/regression-new/issue-1528/2.test.out index bb2c814a11a..3fabbb8ebf9 100644 --- a/pyk/regression-new/issue-1528/2.test.out +++ b/pyk/regression-new/issue-1528/2.test.out @@ -3,6 +3,7 @@ bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> bar ( 0 , 0 ) + ~> .K 1 diff --git a/pyk/regression-new/issue-1528/3.test.out b/pyk/regression-new/issue-1528/3.test.out index 8a6fed85be2..61bc7b553b3 100644 --- a/pyk/regression-new/issue-1528/3.test.out +++ b/pyk/regression-new/issue-1528/3.test.out @@ -3,6 +3,7 @@ bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> bar ( 0 , 1 ) + ~> .K 2 diff --git a/pyk/regression-new/kprove-haskell/sum-spec.k.out b/pyk/regression-new/kprove-haskell/sum-spec.k.out index 85a43a5e1a5..5804c3e0323 100644 --- a/pyk/regression-new/kprove-haskell/sum-spec.k.out +++ b/pyk/regression-new/kprove-haskell/sum-spec.k.out @@ -17,6 +17,7 @@ Subproofs: 0 │ │ addCounter ( N:Int ) │ ~> K_CELL_f6d31965:K +│ ~> .K │ │ │ C:Int @@ -40,6 +41,7 @@ Subproofs: 0 ┃ │ ┃ │ addCounter ( N:Int ) ┃ │ ~> K_CELL_f6d31965:K +┃ │ ~> .K ┃ │ ┃ │ ┃ │ C:Int @@ -60,6 +62,7 @@ Subproofs: 0 ┃ │ ┃ │ addCounter ( N:Int +Int -1 ) ┃ │ ~> K_CELL_f6d31965:K +┃ │ ~> .K ┃ │ ┃ │ ┃ │ C:Int +Int 1 @@ -126,6 +129,7 @@ Subproofs: 0 │ │ addCounter ( N:Int ) │ ~> K_CELL_f6d31965:K + │ ~> .K │ │ │ C:Int diff --git a/pyk/regression-new/kprove-haskell/test-fail-spec.k.out b/pyk/regression-new/kprove-haskell/test-fail-spec.k.out index 436ef76d05e..e0bad9fe2da 100644 --- a/pyk/regression-new/kprove-haskell/test-fail-spec.k.out +++ b/pyk/regression-new/kprove-haskell/test-fail-spec.k.out @@ -21,6 +21,7 @@ Failing nodes: The following cells failed matching individually (antecedent #Implies consequent): K_CELL: doIt ( -3 #Implies 0 ) ~> K_CELL_f6d31965:K + ~> .K Path condition: #Top Failed to generate a model. @@ -32,6 +33,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur │ │ doIt ( -3 ) │ ~> K_CELL_f6d31965:K +│ ~> .K │ │ │ COUNTER_CELL @@ -49,6 +51,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur │ │ doIt ( 0 ) │ ~> K_CELL_f6d31965:K +│ ~> .K │ │ │ COUNTER_CELL diff --git a/pyk/regression-new/kprove-haskell/test-spec.k.out b/pyk/regression-new/kprove-haskell/test-spec.k.out index c9b7ba80a43..4a539a23f03 100644 --- a/pyk/regression-new/kprove-haskell/test-spec.k.out +++ b/pyk/regression-new/kprove-haskell/test-spec.k.out @@ -17,6 +17,7 @@ Subproofs: 0 │ │ doIt ( 3 ) │ ~> K_CELL_f6d31965:K +│ ~> .K │ │ │ COUNTER_CELL @@ -35,6 +36,7 @@ Subproofs: 0 │ │ doIt ( 0 ) │ ~> K_CELL_f6d31965:K +│ ~> .K │ │ │ COUNTER_CELL:Int @@ -55,6 +57,7 @@ Subproofs: 0 doIt ( 0 ) ~> K_CELL_f6d31965:K + ~> .K COUNTER_CELL diff --git a/pyk/regression-new/or-llvm/4.test.out b/pyk/regression-new/or-llvm/4.test.out index 07a934af5b0..4e21e9a6a73 100644 --- a/pyk/regression-new/or-llvm/4.test.out +++ b/pyk/regression-new/or-llvm/4.test.out @@ -2,6 +2,7 @@ 2 ~> test ( foo ~> .K ) + ~> .K 0 diff --git a/pyk/regression-new/or-llvm/5.test.out b/pyk/regression-new/or-llvm/5.test.out index a6231398dd0..c459841dce7 100644 --- a/pyk/regression-new/or-llvm/5.test.out +++ b/pyk/regression-new/or-llvm/5.test.out @@ -2,6 +2,7 @@ 2 ~> test ( bar ~> .K ) + ~> .K 0