test/regress/regress0/bv/issue-4130.smt2


1
2
3
4
5
6
7
8
9
10
11

; REQUIRES: no-competition
; EXPECT: (error "Parse Error: issue-4130.smt2:10.39: expecting bit-width > 0
; EXPECT:
; EXPECT:   (assert (and (= a (bv2nat ((_ int2bv 0) a)))))
; EXPECT:                                        ^
; EXPECT: ")
; EXIT: 1
(set-logic ALL)
(declare-fun a () Int)
(assert (and (= a (bv2nat ((_ int2bv 0) a)))))
(check-sat)