diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-04 16:16:02 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-04 16:16:02 +0000 |
| commit | 842c5e7e08bf21980b34e40112e15a16cb18aee2 (patch) | |
| tree | d10e23e48a2f2910c6ff6ee256835cd9ee254954 /test | |
| parent | 7094d127b0cd69b4926203c05dd2d60cb4d27292 (diff) | |
also add test case
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/push-pop/incremental-subst-bug.cvc | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc new file mode 100644 index 000000000..b9936bfa4 --- /dev/null +++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc @@ -0,0 +1,22 @@ +% 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; +% EXIT: 10 |