blob: d0c9aeedc26d58596a9a8e4928964e04ed4f1c05 (
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
26
27
|
; COMMAND-LINE: --strings-fmf
; EXPECT: sat
(set-logic QF_S)
(declare-fun a () String)
(declare-fun b () Int)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () Bool)
(declare-fun j () String)
(declare-fun k () String)
(assert (= e "0000000000"))
(assert (distinct a d))
(assert
(ite (distinct b 0)
(and (= (str.++ d e) (str.++ c j))
(= (str.len c) 2)
(= j (str.++ f k))
(= f (str.++ g h))
(str.in_re g (str.to_re "A")))
(str.in_re j (str.to_re ""))))
(assert (distinct i (= b 0)))
(assert i)
(check-sat)
|
