summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/re.all.smt2
blob: 01d57a6e133cb883ee5eeaab8d7582be54b91df0 (plain)
1
2
3
4
5
6
7
; COMMAND-LINE: --strings-exp
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-const x String)
(assert (str.in_re x (re.++ (str.to_re "abc") re.all)))
(assert (not (str.prefixof "abc" x)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback