blob: a228194f4f858c1430bd082c5b2ed463db71ce63 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
include "Includee.dfy"
method test_include(z:int)
{
// Make sure we can still see function bodies
assert forall y :: f(y) == 2*y;
// Use an unverified method
var w := m_unproven(z);
assert w == 2*z;
}
|