Add tests that enumerate and verify rewrite rules (#2344)

1 files changed, 25 insertions, 0 deletions

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)