Skip to content

Commit 4431b20

Browse files
theo25theo25
committed
update lit tests
1 parent e9e71dc commit 4431b20

File tree

109 files changed

+11771
-20920
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

109 files changed

+11771
-20920
lines changed

‎test/output/add-rewrite/input.proof.debug.out.diff

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,12 @@ hook result: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Stat
1616
function: Lblproject'Coln'KItem{} (0:0)
1717
rule: 153 1 [] []
1818
VarK = kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
19-
tail_call_info: apply_rule_153 notail
20-
tail_call_info: apply_rule_112 notail
19+
function exit: 153 notail
20+
function exit: 112 notail
2121
function: LblinitGeneratedCounterCell{} (1)
2222
rule: 110 0 [] []
23-
tail_call_info: apply_rule_110 notail
24-
tail_call_info: apply_rule_111 notail
23+
function exit: 110 notail
24+
function exit: 111 notail
2525
config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
2626
rule: 107 5 [ADD-REWRITE.state-next] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:18]
2727
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]

‎test/output/add-rewrite/input.proof.out.diff

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,12 @@ hook result: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Stat
1616
function: Lblproject'Coln'KItem{} (0:0)
1717
rule: 153 1
1818
VarK = kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
19-
tail_call_info: apply_rule_153 notail
20-
tail_call_info: apply_rule_112 notail
19+
function exit: 153 notail
20+
function exit: 112 notail
2121
function: LblinitGeneratedCounterCell{} (1)
2222
rule: 110 0
23-
tail_call_info: apply_rule_110 notail
24-
tail_call_info: apply_rule_111 notail
23+
function exit: 110 notail
24+
function exit: 111 notail
2525
config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
2626
rule: 107 5
2727
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]

‎test/output/arith/add.proof.out.diff

Lines changed: 11 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -16,42 +16,40 @@ hook result: kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp
1616
function: Lblproject'Coln'KItem{} (0:0)
1717
rule: 2877 1
1818
VarK = kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2")))]
19-
tail_call_info: apply_rule_2877 notail
20-
tail_call_info: apply_rule_2804 notail
19+
function exit: 2877 notail
20+
function exit: 2804 notail
2121
function: LblinitGeneratedCounterCell{} (1)
2222
rule: 2802 0
23-
tail_call_info: apply_rule_2802 notail
24-
tail_call_info: apply_rule_2803 notail
23+
function exit: 2802 notail
24+
function exit: 2803 notail
2525
config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
2626
side condition entry: 2746 1
2727
VarHOLE = kore[\dv{SortInt{}}("1")]
2828
function: LblisKResult{} (1:0)
2929
rule: 2841 1
3030
VarKResult = kore[\dv{SortInt{}}("1")]
31-
tail_call_info: apply_rule_2841 notail
31+
function exit: 2841 notail
3232
hook: BOOL.not LblnotBool'Unds'{} (1)
3333
arg: kore[\dv{SortBool{}}("true")]
3434
hook result: kore[\dv{SortBool{}}("false")]
3535
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
3636
arg: kore[\dv{SortBool{}}("true")]
3737
arg: kore[\dv{SortBool{}}("false")]
3838
hook result: kore[\dv{SortBool{}}("false")]
39-
tail_call_info: side_condition_2746 notail
4039
side condition exit: 2746 false
4140
side condition entry: 2747 1
4241
VarHOLE = kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))]
4342
function: LblisKResult{} (1:0)
4443
rule: 2840 1
4544
VarK = kore[kseq{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2")),dotk{}())]
46-
tail_call_info: apply_rule_2840 notail
45+
function exit: 2840 notail
4746
hook: BOOL.not LblnotBool'Unds'{} (1)
4847
arg: kore[\dv{SortBool{}}("false")]
4948
hook result: kore[\dv{SortBool{}}("true")]
5049
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
5150
arg: kore[\dv{SortBool{}}("true")]
5251
arg: kore[\dv{SortBool{}}("true")]
5352
hook result: kore[\dv{SortBool{}}("true")]
54-
tail_call_info: side_condition_2747 notail
5553
side condition exit: 2747 true
5654
rule: 2747 4
5755
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
@@ -63,30 +61,28 @@ side condition entry: 2746 1
6361
function: LblisKResult{} (1:0)
6462
rule: 2841 1
6563
VarKResult = kore[\dv{SortInt{}}("1")]
66-
tail_call_info: apply_rule_2841 notail
64+
function exit: 2841 notail
6765
hook: BOOL.not LblnotBool'Unds'{} (1)
6866
arg: kore[\dv{SortBool{}}("true")]
6967
hook result: kore[\dv{SortBool{}}("false")]
7068
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
7169
arg: kore[\dv{SortBool{}}("true")]
7270
arg: kore[\dv{SortBool{}}("false")]
7371
hook result: kore[\dv{SortBool{}}("false")]
74-
tail_call_info: side_condition_2746 notail
7572
side condition exit: 2746 false
7673
side condition entry: 2747 1
7774
VarHOLE = kore[\dv{SortInt{}}("2")]
7875
function: LblisKResult{} (1:0)
7976
rule: 2841 1
8077
VarKResult = kore[\dv{SortInt{}}("2")]
81-
tail_call_info: apply_rule_2841 notail
78+
function exit: 2841 notail
8279
hook: BOOL.not LblnotBool'Unds'{} (1)
8380
arg: kore[\dv{SortBool{}}("true")]
8481
hook result: kore[\dv{SortBool{}}("false")]
8582
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
8683
arg: kore[\dv{SortBool{}}("true")]
8784
arg: kore[\dv{SortBool{}}("false")]
8885
hook result: kore[\dv{SortBool{}}("false")]
89-
tail_call_info: side_condition_2747 notail
9086
side condition exit: 2747 false
9187
rule: 2748 4
9288
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
@@ -102,12 +98,11 @@ side condition entry: 2740 1
10298
function: LblisKResult{} (1)
10399
rule: 2841 1
104100
VarKResult = kore[\dv{SortInt{}}("3")]
105-
tail_call_info: apply_rule_2841 notail
101+
function exit: 2841 notail
106102
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
107103
arg: kore[\dv{SortBool{}}("true")]
108104
arg: kore[\dv{SortBool{}}("true")]
109105
hook result: kore[\dv{SortBool{}}("true")]
110-
tail_call_info: side_condition_2740 notail
111106
side condition exit: 2740 true
112107
rule: 2740 5
113108
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
@@ -120,30 +115,28 @@ side condition entry: 2746 1
120115
function: LblisKResult{} (1:0)
121116
rule: 2841 1
122117
VarKResult = kore[\dv{SortInt{}}("1")]
123-
tail_call_info: apply_rule_2841 notail
118+
function exit: 2841 notail
124119
hook: BOOL.not LblnotBool'Unds'{} (1)
125120
arg: kore[\dv{SortBool{}}("true")]
126121
hook result: kore[\dv{SortBool{}}("false")]
127122
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
128123
arg: kore[\dv{SortBool{}}("true")]
129124
arg: kore[\dv{SortBool{}}("false")]
130125
hook result: kore[\dv{SortBool{}}("false")]
131-
tail_call_info: side_condition_2746 notail
132126
side condition exit: 2746 false
133127
side condition entry: 2747 1
134128
VarHOLE = kore[\dv{SortInt{}}("3")]
135129
function: LblisKResult{} (1:0)
136130
rule: 2841 1
137131
VarKResult = kore[\dv{SortInt{}}("3")]
138-
tail_call_info: apply_rule_2841 notail
132+
function exit: 2841 notail
139133
hook: BOOL.not LblnotBool'Unds'{} (1)
140134
arg: kore[\dv{SortBool{}}("true")]
141135
hook result: kore[\dv{SortBool{}}("false")]
142136
hook: BOOL.and Lbl'Unds'andBool'Unds'{} ()
143137
arg: kore[\dv{SortBool{}}("true")]
144138
arg: kore[\dv{SortBool{}}("false")]
145139
hook result: kore[\dv{SortBool{}}("false")]
146-
tail_call_info: side_condition_2747 notail
147140
side condition exit: 2747 false
148141
rule: 2748 4
149142
Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]

0 commit comments

Comments
 (0)