1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy
new file mode 100644
index 000000000..6c6da3dd2
--- /dev/null
+++ b/test/regress/regress1/rr-verify/regex.sy
@@ -0,0 +1,32 @@
+; 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 SLIA)
+
+(synth-fun f ((x String) (y String)) Bool (
+
+(Start Bool (
+  true
+  false
+  (= StartStr StartStr)
+  (str.in.re StartStr StartRe)
+))
+
+(StartRe RegLan (
+  re.allchar
+  (re.++ StartRe StartRe)
+  (re.union StartRe StartRe)
+  (re.* StartRe)
+  (str.to.re StartStr)
+))
+
+(StartStr String (
+  x y "A" "B" ""
+  (str.++ StartStr StartStr)
+))
+
+))
+
+(check-synth)