Reduced example from pcc's bug report.

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index fcae3196abd97abd689830a34fd45f72b1fe55aa..dcc44d43aae82f8f2503f208ea530876df7d2c9a 100644 (file)
--- 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 (file)
index 0000000..4dc1cc2
--- /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)