From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 4 Oct 2011 16:16:02 +0000 (+0000)
Subject: also add test case
X-Git-Tag: cvc5-1.0.0~8427
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=842c5e7e08bf21980b34e40112e15a16cb18aee2;p=cvc5.git

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