summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/issue-4075.smt2
blob: 083fbf897ee26b0463a59fcad5a096b465630c51 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; REQUIRES: no-competition
; EXPECT: (error "Parse Error: issue-4075.smt2:11.26: expecting number of repeats > 0
; EXPECT:
; EXPECT:  (simplify ((_ repeat 0) b))
; EXPECT:                       ^
; EXPECT:")
; EXIT: 1
(set-logic QF_BV)
(define-sort a () (_ BitVec 4))
(declare-const b a)
(simplify ((_ repeat 0) b))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback