Add regex grammar to rewriter verification tests (#2426)

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 39a7a4f4dadba3688483b89420c225e96863ef06..b8b047e6d36845b25847026898e36be9c96ae524 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1401,6 +1401,7 @@ REG1_TESTS = \
        regress1/rr-verify/bool-crci.sy \
        regress1/rr-verify/bv-term-32.sy \
        regress1/rr-verify/bv-term.sy \
+       regress1/rr-verify/regex.sy \
        regress1/rr-verify/string-term.sy \
        regress1/sep/chain-int.smt2 \
        regress1/sep/crash1220.smt2 \

diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy
new file mode 100644 (file)
index 0000000..6c6da3d
--- /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)