From 8227a1fac2ce875dfed79c4b6cc8499158e4d7d1 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sun, 6 Apr 2014 18:57:53 -0400
Subject: Reduced example from pcc's bug report.

---
 test/regress/regress0/unconstrained/Makefile.am | 1 +
 test/regress/regress0/unconstrained/ite.smt2    | 9 +++++++++
 2 files changed, 10 insertions(+)
 create mode 100644 test/regress/regress0/unconstrained/ite.smt2

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index fcae3196a..dcc44d43a 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -65,6 +65,7 @@ TESTS =	\
 	bvult.smt2 \
 	geq.smt2 \
 	gt.smt2 \
+	ite.smt2 \
 	leq.smt2 \
 	lt.smt2 \
 	uf1.smt2 \
diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2
new file mode 100644
index 000000000..4dc1cc295
--- /dev/null
+++ b/test/regress/regress0/unconstrained/ite.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_AUFBV )
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun a () (Array U (_ BitVec 64) ) )
+(declare-fun i () U)
+(declare-fun p () Bool)
+(assert (= (_ bv0 64) (ite p (select a i) (_ bv1 64))))
+(check-sat)
+(exit)
-- 
cgit v1.2.3