test/regress/regress1/strings/ilc-l-nt.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14

(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(set-option :strings-exp true)
 
(declare-fun s () String)
(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))
 
(declare-fun target () String)
(assert (or (= target "l") (= target "m")))
 
(declare-fun location () Int)
(assert (= (* 2 location) (str.indexof s target 0)))
 
(check-sat)