1(benchmark bitvec2.smt
2  :source {
3Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
4Contributed by Vijay Ganesh (vganesh@stanford.edu).  Translated into SMT-LIB
5format by Clark Barrett using CVC3.
6
7}
8  :status unsat
9  :difficulty { 0 }
10  :category { crafted }
11  :logic QF_BV
12  :extrapreds ((a))
13  :formula
14(not (= (concat bv1[1] (ite a bv0[1] bv1[1])) (ite a bv2[2] bv3[2])))
15)
16