summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/large-model.smt2
blob: ca52e816bfd8552824f2843b037030e39c413e9e (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --lang=smt2.6.1 --check-models
; EXPECT: (error "Cannot generate model with string whose length exceeds UINT32_MAX")
; EXIT: 1
(set-logic SLIA)
(declare-fun x () String)
(assert (> (str.len x) 100000000000000000000000000000000000000000000000000))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback