summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2
blob: b513494b8d13ebc3e357a327fa933299bcf4b55e (plain) 
1
2
3
4
5
6
7
8
9

(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-option :strings-exp true)

(declare-fun s () String)

(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0)))))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback