blob: 8f6593148c1a146953d454eab5c03a60f38b504b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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)
|
