From 6a6630bf6fa4b68c6a483b767be4c696da8fd0bd Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Nov 2014 16:16:57 -0500
Subject: Corrected fix for missing case in model postprocessor (resolves bug
 #595).

---
 test/regress/regress0/Makefile.am | 3 ++-
 test/regress/regress0/bug595.cvc  | 7 +++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/bug595.cvc

(limited to 'test')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c0ee0f2bb..15888fbce 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -166,7 +166,8 @@ BUG_TESTS = \
 	bug576a.smt2 \
 	bug578.smt2 \
 	bug585.cvc \
-	bug586.cvc
+	bug586.cvc \
+	bug595.cvc
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc
new file mode 100644
index 000000000..c11cfb6e4
--- /dev/null
+++ b/test/regress/regress0/bug595.cvc
@@ -0,0 +1,7 @@
+% EXPECT: sat
+
+f : INT -> [# i:INT, b:INT #];
+a : INT;
+ASSERT f(a) /= (# i := 0, b := 0 #);
+
+CHECKSAT;
-- 
cgit v1.2.3