test/regress/regress0/push-pop/incremental-subst-bug.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

% COMMAND-LINE: --incremental
U : TYPE;
x, y : U;
% EXPECT: invalid
QUERY x = y;
ASSERT x = y;
% EXPECT: valid
QUERY x = y;
PUSH;
z : U;
% EXPECT: valid
QUERY x = y;
% EXPECT: invalid
QUERY x = z;
% EXPECT: invalid
QUERY z = x;
% EXPECT: invalid
QUERY z /= x;
POP;
% EXPECT: invalid
QUERY z /= x;