diff options
| -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 |