1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy
new file mode 100644
index 000000000..da7d98e66
--- /dev/null
+++ b/test/regress/regress1/sygus/cube-nia.sy
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic NIA)
+
+(synth-fun cube ((x Int)) Int
+  (
+    (Start Int (ntInt))
+  
+    (ntBool Bool
+      ( 
+        (> ntInt ntInt)
+        (= ntInt ntInt)
+      )
+    )
+    (ntInt Int
+      (1 x
+        (* ntInt ntInt)
+        (ite ntBool ntInt ntInt)
+      )
+    )
+  )
+)
+
+(constraint (= (cube 1) 1))
+(constraint (= (cube 2) 8))
+(check-synth)