summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers/tpp-unit-fail-qbv.smt2
blob: 2ef929551b5cbedb20da120e44a92ecc6c9f48f3 (plain) 
1
2
3
4
5
6
7
8

(set-logic BV)
(set-info :status unsat)
(declare-fun t () (_ BitVec 4))
(declare-fun s () (_ BitVec 4))
(assert
(distinct (bvult t (bvnot (bvneg s))) (exists ((BOUND_VARIABLE_273 (_ BitVec 4))) (bvugt (bvurem BOUND_VARIABLE_273 s) t)))
)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback