From 842c5e7e08bf21980b34e40112e15a16cb18aee2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 4 Oct 2011 16:16:02 +0000
Subject: [PATCH] also add test case

---
 .../push-pop/incremental-subst-bug.cvc        | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 test/regress/regress0/push-pop/incremental-subst-bug.cvc

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
-- 
2.30.2