blob: a02fbc5ce0e4efb6d1634e0007122f7b92855162 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-inference --strings-exp -q
(set-logic ALL)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun f () String)
(declare-fun e () String)
(assert
(not
(=
(str.contains
c
(str.replace d (str.substr b 0 (str.len d)) "A")
)
(str.contains c "A")
)
)
)
(assert (= a (str.++ c f)))
(assert (= b (str.++ d e)))
(check-sat)
|
