adding regressions (#1925)

1 files changed, 37 insertions, 0 deletions

diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
new file mode 100644
index 000000000..4b0cefcda
--- /dev/null
+++ b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-out=status
+(set-logic BV)
+
+(synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)
+  (
+    (Start (BitVec 64)
+      (#x0000000000000000 #x0000000000000001 x y
+        (bvnot Start)
+        (bvand Start Start)
+        (bvor Start Start)
+        (bvxor Start Start)
+        (bvadd Start Start)
+        (ite CBool Start Start)
+        )
+      )
+    (CBool Bool
+      (true false
+        (and CBool CBool)
+        (or CBool CBool)
+        (not CBool)
+        (bvule Start Start)
+        (= Start Start)
+        )
+      )
+    )
+  )
+
+(declare-var x (BitVec 64))
+(declare-var y (BitVec 64))
+
+(constraint (= (f #x0000000000000000 #x0000000000000001) #x0000000000000000))
+(constraint (= (f #x0000000000000000 #x0000000000000000) #x0000000000000001))
+(constraint (= (f #x0000000000000001 y) y))
+(constraint (= (f #x0000000000000002 #x0000000000000001) #x0000000000000000))
+
+(check-synth)