1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy
new file mode 100644
index 000000000..6c5c1a97b
--- /dev/null
+++ b/test/regress/regress1/sygus/list-head-x.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
+
+(synth-fun f ((x Int)) List)
+
+(declare-var x Int)
+
+(constraint (is-cons (f x)))
+(constraint (= (head (f x)) (+ x 7)))
+(check-synth)