From: Tim King <taking@cs.nyu.edu>
Date: Sun, 6 Apr 2014 22:57:53 +0000 (-0400)
Subject: Reduced example from pcc's bug report.
X-Git-Tag: cvc5-1.0.0~6981^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8227a1fac2ce875dfed79c4b6cc8499158e4d7d1;p=cvc5.git

Reduced example from pcc's bug report.
---

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)