Skip to content

Commit 7ec6841

Browse files
rv-jenkinsttuegel
andauthored
Update dependency: deps/k_release (#2203)
* deps/k_release: v5.0.0-2cbe065 * test/itp-nth-ancestor/nth2-spec.k: missing simplification attribute * test/itp-nth-ancestor: use claim keyword Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
1 parent 289f9d5 commit 7ec6841

File tree

3 files changed

+7
-7
lines changed

3 files changed

+7
-7
lines changed

deps/k_release

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
v5.0.0-fec1350
1+
v5.0.0-2cbe065

test/itp-nth-ancestor/nth1-spec.k

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ require "chain.k"
2929
module NTH1-SPEC
3030
imports V
3131

32-
rule
32+
claim
3333
<g> nth(1, B1, B2) => B1 <~* B2 </g>
3434
<p> .Map => ?_ </p>
3535
<k> apply("nth.e")
@@ -41,7 +41,7 @@ module NTH1-SPEC
4141
~> apply("<~*.i")
4242
=> . </k>
4343

44-
rule
44+
claim
4545
<k> apply("lemma") => . ... </k>
4646
<g> B1 == B2 and B2 <~ B3 => B1 <~ B3 </g>
4747
[trusted]

test/itp-nth-ancestor/nth2-spec.k

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ require "chain.k"
2929
module NTH2-SPEC
3030
imports V
3131

32-
rule
32+
claim
3333
<g> nth(k(N) +Int 1, B1, B2) => B1 <~* B2 </g>
3434
<p> .Map => ?_ </p>
3535
<k> apply("nth.e")
@@ -42,7 +42,7 @@ module NTH2-SPEC
4242
requires k(N) >Int 0 andBool const(N)
4343

4444
// induction hypothesis
45-
rule
45+
claim
4646
<k> apply("ih") => . ... </k>
4747
<g> nth(k(N), B1, B2) => B1 <~* B2 </g>
4848
requires k(N) >Int 0 andBool const(N)
@@ -57,7 +57,7 @@ module NTH2-SPEC
5757
by apply/connect1.
5858
Qed.
5959
*/
60-
rule
60+
claim
6161
<k> apply("lemma") => . ... </k>
6262
<g> B1 <~* B2 and B2 <~ B3 => B1 <~* B3 </g>
6363
[trusted]
@@ -70,5 +70,5 @@ module V
7070

7171
syntax Int ::= k(Int) [function, functional, injective, smtlib(k)]
7272

73-
rule (k(N) +Int 1) -Int 1 => k(N)
73+
rule (k(N) +Int 1) -Int 1 => k(N) [simplification]
7474
endmodule

0 commit comments

Comments
 (0)