1 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy
new file mode 100644
index 000000000..1e810fea3
--- /dev/null
+++ b/test/regress/regress1/sygus/cegisunif-depth1.sy
@@ -0,0 +1,34 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-out=status
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  (
+    (Start Int
+      (0 1 x y
+        (+ Start Start)
+        (- Start Start)
+        (ite CBool Start Start)
+        )
+      )
+    (CBool Bool
+      (true false
+        (and CBool CBool)
+        (or CBool CBool)
+        (not CBool)
+        (<= Start Start)
+        ; Having equality makes the problem easy to CEGIS
+        ; (= Start Start)
+        )
+      )
+    )
+  )
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f 0 1) 0))
+(constraint (= (f 1 y) y))
+(constraint (= (f 2 1) 0))
+
+(check-synth)