summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2
blob: 61f7929992b2381d6cde9c4fd853df40039122c5 (plain) 
1
2
3
4
5
6
7

; EXPECT: (error "Parse Error: issue4437-unc-quant.smt2:6.15: Quantifier used in non-quantified logic.")
; EXIT: 1
(set-logic QF_AUFBVLIA)
(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(assert (forall ((c (_ BitVec 8))) (= (bvashr c a) b)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback