Skip to content

Commit dc8f0c9

Browse files
authored
add test for silver issue 688 (#694)
1 parent 2e0c91e commit dc8f0c9

1 file changed

Lines changed: 24 additions & 0 deletions

File tree

  • src/test/resources/all/issues/silver
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
adt Unit {
2+
unit()
3+
}
4+
5+
domain Exe67 {
6+
function F67(x : Int, y : Int) : Int
7+
8+
function L67() : Int
9+
function R67() : Int
10+
11+
axiom LeftUnit67 {
12+
forall x : Int :: {F67(L67(), x)} F67(L67(), x) == L67()
13+
}
14+
15+
axiom RightUnit67 {
16+
forall x : Int :: {F67(x, R67())} F67(x, R67()) == R67()
17+
}
18+
}
19+
20+
function functionUnit(x : Int) : Unit
21+
22+
function lemmaLEqualR67() : Unit
23+
ensures L67() == R67()
24+
{let x == (F67(L67(), R67())) in unit() }

0 commit comments

Comments
 (0)