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