From 557d4c2d3dd0f9f0210b9438c952903635248357 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 12:42:18 +0000
Subject: remove an obsolete (and incorrect) assertion in boolean-terms; also
 add failing regression for bug 472

---
 test/regress/regress0/bug472.smt2 | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test/regress/regress0/bug472.smt2

(limited to 'test/regress')

diff --git a/test/regress/regress0/bug472.smt2 b/test/regress/regress0/bug472.smt2
new file mode 100644
index 000000000..7af988ec3
--- /dev/null
+++ b/test/regress/regress0/bug472.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_AUFLIA)
+(set-option :produce-models true)
+(declare-fun a () (Array Int Int))
+(assert (= (select a 0) 0))
+(check-sat)
+(get-value (a))
+(assert (= a @1))
+(check-sat)
-- 
cgit v1.2.3