summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/eager-force-logic.smt2
blob: 9b7dee8c23e51d263f716097ec7c3f3f0306f6b3 (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --bitblast=eager --force-logic="QF_BV"
; EXPECT: sat
(set-option :produce-models true)
(declare-fun a () (_ BitVec 16))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))

(assert (bvult a (bvadd b c)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback