From 4f219fd2d97ab61c2060e3340ec468f35d99cbdf Mon Sep 17 00:00:00 2001
From: rv-jenkins <admin@runtimeverification.com>
Date: Fri, 8 Sep 2023 05:03:27 -0600
Subject: [PATCH] Update dependency: deps/k_release (#3636)

---
 deps/k_release                                    |  2 +-
 test/imp/imp.k                                    | 10 +++++-----
 test/kprove/imp.k                                 | 10 +++++-----
 test/map-symbolic/assignment-11-spec.k.out.golden |  4 ++--
 test/smc/smc.k                                    |  8 ++++----
 5 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/deps/k_release b/deps/k_release
index 290c47f4a5..452ca39512 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-6.0.36
+6.0.87
diff --git a/test/imp/imp.k b/test/imp/imp.k
index acdce0966a..70c14f2d6a 100644
--- a/test/imp/imp.k
+++ b/test/imp/imp.k
@@ -151,8 +151,8 @@ considering their erasure as computational steps in the resulting transition
 systems.  You can make these rules computational (dropping the attribute
 \texttt{structural}) if you do want these to count as computational steps. */
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
 /*@ \subsubsection{Assignment}
 The assigned variable is updated in the state.  The variable is expected
@@ -172,7 +172,7 @@ and counting only the steps corresponding to computational rules as
 transitions (i.e., hiding the structural rules as unobservable, or
 internal steps). */
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
 /*@ \subsubsection{Conditional}
 The conditional statement has two semantic cases, corresponding to
@@ -188,7 +188,7 @@ argument is allowed to be evaluated. */
 We give the semantics of the \texttt{while} loop by unrolling.
 Note that we preferred to make the rule below structural. */
 
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
 /*@ \subsection{Programs}
 The semantics of an IMP program is that its body statement is executed
@@ -205,7 +205,7 @@ a computational step. */
 
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
   // for add-spec, double-sum-spec, run-stepf-repl-scrip-spec, sum-div-spec
   // , sum-save-proofs-spec
diff --git a/test/kprove/imp.k b/test/kprove/imp.k
index 75646232fa..53d82a442b 100644
--- a/test/kprove/imp.k
+++ b/test/kprove/imp.k
@@ -151,8 +151,8 @@ considering their erasure as computational steps in the resulting transition
 systems.  You can make these rules computational (dropping the attribute
 \texttt{structural}) if you do want these to count as computational steps. */
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
 /*@ \subsubsection{Assignment}
 The assigned variable is updated in the state.  The variable is expected
@@ -172,7 +172,7 @@ and counting only the steps corresponding to computational rules as
 transitions (i.e., hiding the structural rules as unobservable, or
 internal steps). */
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
 /*@ \subsubsection{Conditional}
 The conditional statement has two semantic cases, corresponding to
@@ -188,7 +188,7 @@ argument is allowed to be evaluated. */
 We give the semantics of the \texttt{while} loop by unrolling.
 Note that we preferred to make the rule below structural. */
 
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
 /*@ \subsection{Programs}
 The semantics of an IMP program is that its body statement is executed
@@ -205,7 +205,7 @@ a computational step. */
 
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
 //
 // verification ids
diff --git a/test/map-symbolic/assignment-11-spec.k.out.golden b/test/map-symbolic/assignment-11-spec.k.out.golden
index 7cecdc5572..c4f7bfe07c 100644
--- a/test/map-symbolic/assignment-11-spec.k.out.golden
+++ b/test/map-symbolic/assignment-11-spec.k.out.golden
@@ -12,8 +12,8 @@
 #And
   <k>
     assignmentResult ( ( MAP
-    X:MyId |-> 1
-    Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .
+    X:MyId |-> 1 ) [ Z:MyId <- 3 ]
+    Y:MyId |-> 2 ) ~> .
   </k>
 #And
   {
diff --git a/test/smc/smc.k b/test/smc/smc.k
index 22c4c05628..c8e7c29e1c 100644
--- a/test/smc/smc.k
+++ b/test/smc/smc.k
@@ -81,15 +81,15 @@ module SMC
   rule <k> && E => E ...</k>
        <stack> true : S:ValStack => S </stack>
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
   rule X:Id = E:AExp ; => E ~> X =
   rule <k> X = => . ...</k>
        <mem>... X |-> (_ => I) ...</mem>
        <stack> I:Int : S:ValStack => S </stack>
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
   rule if (B:BExp) S1:Block else S2:Block  => B ~> choice(S1,S2)
   rule <k> choice(Bl,_) => Bl ...</k> <stack> true : S:ValStack => S </stack>
@@ -99,7 +99,7 @@ module SMC
 
   rule <k> int (X,Xs => Xs);_ </k> <mem> Rho:Map (.Map => X|->0) </mem>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
   // for add-spec, add-stack-spec, double-sum-spec, double-sum-stack-spec,
   // sum-spec, sum-stack-spec