blob: e50e035f330fdd311ad588cbad757ed581699d13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic ALL)
(set-option :sygus-inference true)
(set-info :status sat)
(declare-fun a () String)
(declare-fun b () String)
(declare-const c String)
(declare-const d String)
(declare-fun g () Bool)
(declare-fun e () Bool)
(declare-fun f () String)
(assert (str.in_re (str.substr a 0 (str.len (str.substr a 0 (str.len (str.substr a 0 (str.len c)))))) (re.* (re.++ (str.to_re "") (re.* (str.to_re "aa"))))))
(assert (str.in_re (str.substr b 0 (str.len d)) (re.* (re.++ (re.* (str.to_re "")) (str.to_re "bb")))))
(assert (= 4 (str.len d)))
(assert (not (= (str.substr a 0 (str.len c)) d)))
(assert (= g (not (= "file" (str.substr a (str.len c) (str.len f))))))
(assert (= e (not g)))
(assert e)
(check-sat)
|
