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

; COMMAND-LINE: --lang=smt2.6 --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