4 files changed, 116 insertions, 0 deletions
diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy
new file mode 100644
index 000000000..955245f87
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bool-crci.sy
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool 
+ ((Start Bool (
+   (and depth1 depth1)
+   (not depth1)
+   (or depth1 depth1)
+   (xor depth1 depth1)
+ ))
+ (depth1 Bool (
+   (and depth2 depth2)
+   (not depth2)
+   (or depth2 depth2)
+   (xor depth2 depth2)
+   x
+ ))
+ (depth2 Bool (
+   (and depth3 depth3)
+   (not depth3)
+   (or depth3 depth3)
+   (xor depth3 depth3)
+   w
+ ))
+ (depth3 Bool (
+   (and depth4 depth4)
+   (not depth4)
+   (or depth4 depth4)
+   (xor depth4 depth4)
+   y
+ ))
+ (depth4 Bool (
+   z
+ )))
+)
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
new file mode 100644
index 000000000..6c07bd8aa
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ((s (BitVec 32)) (t (BitVec 32))) (BitVec 32)
+  (
+   (Start (BitVec 32) (
+     s
+     t
+     #x00000000
+     (bvneg  Start)
+     (bvnot  Start)
+     (bvadd  Start Start)
+     (bvmul  Start Start)
+     (bvand  Start Start)
+     (bvlshr Start Start)
+     (bvor   Start Start)
+     (bvshl  Start Start)
+   ))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
new file mode 100644
index 000000000..025479f24
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ((s (BitVec 4)) (t (BitVec 4))) (BitVec 4)
+  (
+   (Start (BitVec 4) (
+     s
+     t
+     #x0
+     (bvneg  Start)
+     (bvnot  Start)
+     (bvadd  Start Start)
+     (bvmul  Start Start)
+     (bvand  Start Start)
+     (bvlshr Start Start)
+     (bvor   Start Start)
+     (bvshl  Start Start)
+   ))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy
new file mode 100644
index 000000000..8f6593148
--- /dev/null
+++ b/test/regress/regress1/rr-verify/string-term.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic SLIA)
+
+(synth-fun f ((x String) (y String) (z Int)) String (
+(Start String (
+  x y "A" "B" ""
+  (str.++ Start Start)
+  (str.replace Start Start Start)
+  (str.at Start StartInt)
+  (int.to.str StartInt)
+  (str.substr Start StartInt StartInt)))
+(StartInt Int (
+  0 1 z
+  (+ StartInt StartInt)
+  (- StartInt StartInt)
+  (str.len Start)
+  (str.to.int Start)
+  (str.indexof Start Start StartInt)))
+))
+
+(check-synth)