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

; EXPECT: (error "Parse Error: issue-4075.smt2:10.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