1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy
new file mode 100644
index 000000000..b3d950436
--- /dev/null
+++ b/test/regress/regress1/sygus/array-uc.sy
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort U 0)
+(synth-fun f ((x (Array U Int)) (y U)) Bool)
+
+(declare-var x (Array U Int))
+(declare-var y U)
+
+(constraint (= (f (store x y 0) y) true))
+(constraint (= (f (store x y 1) y) false))
+
+; f can be (= (select x y) 0)
+(check-synth)