Test/test2/FormulaTerm2.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file has been created to test some of the formula/term issues in Zap.
// However, the test harness does not specify any particular prover to be used,
// since these tests should pass regardless of which prover is used.

procedure P()
{
  var a: int, b: int, t: bool;

  start:
    assume a == b;
    t := a == b;
    assert t;
    return;
}

function f(bool) returns (int);
const A: int;
const B: int;

axiom f(A < B) == 5;

procedure Q()
{
  start:
    assume A < B;
    assert f(true) == 5;
    return;
}

// ----- and now some erroneous procedures

procedure PX()
{
  var a: int, b: int, t: bool;

  start:
    assume a == b;
    t := a == b;
    assert !t;  // error
    return;
}

procedure QX()
{
  start:
    assume A < B;
    assert f(true) < 2;  // error
    return;
}