also add test case

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 (file)
index 0000000..b9936bf
--- /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