adding regressions (#1925)

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 7784a68258b192ae569d59e24d177fc01bfb9386..c0f1cf315b531184a09568215937cfbfb15bbd57 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1470,6 +1470,7 @@ REG1_TESTS = \
        regress1/sygus/array_search_2.sy \
        regress1/sygus/array_sum_2_5.sy \
        regress1/sygus/cegar1.sy \
+       regress1/sygus/cegisunif-depth1.sy \
        regress1/sygus/cggmp.sy \
        regress1/sygus/clock-inc-tuple.sy \
        regress1/sygus/commutative.sy \
@@ -1590,6 +1591,7 @@ REG2_TESTS = \
        regress2/strings/norn-dis-0707-3.smt2 \
        regress2/sygus/MPwL_d1s3.sy \
        regress2/sygus/array_sum_dd.sy \
+       regress2/sygus/cegisunif-depth1-bv.sy \
        regress2/sygus/ex23.sy \
        regress2/sygus/icfp_easy_mt_ite.sy \
        regress2/sygus/inv_gen_n_c11.sy \

diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy
new file mode 100644 (file)
index 0000000..1e810fe
--- /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)

diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy
new file mode 100644 (file)
index 0000000..4b0cefc
--- /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)