1(benchmark bitvec1.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 :extrafuns ((a BitVec[32])) 13 :extrafuns ((b BitVec[32])) 14 :extrafuns ((c BitVec[32])) 15 :extrafuns ((res BitVec[32])) 16 :formula 17(flet ($cvc_1 (= (extract[0:0] a) bv1[1])) (flet ($cvc_2 (= (extract[0:0] b) bv1[1])) (let (?cvc_0 (extract[0:0] c)) (flet ($cvc_6 (= ?cvc_0 bv1[1])) (let (?cvc_3 (extract[0:0] res)) (flet ($cvc_4 (= (extract[1:1] a) bv1[1])) (flet ($cvc_5 (= (extract[1:1] b) bv1[1])) (flet ($cvc_8 (if_then_else $cvc_4 (not $cvc_5) $cvc_5)) (let (?cvc_7 (extract[1:1] c)) (let (?cvc_9 (extract[1:1] res)) (not (implies (and (and (and (= (extract[1:0] a) bv1[2]) (= (extract[1:0] b) bv1[2])) (and (if_then_else (and $cvc_1 $cvc_2) $cvc_6 (= ?cvc_0 bv0[1])) (if_then_else (if_then_else $cvc_1 (not $cvc_2) $cvc_2) (= ?cvc_3 bv1[1]) (= ?cvc_3 bv0[1])))) (and (if_then_else (or (and $cvc_4 $cvc_5) (and $cvc_8 $cvc_6) ) (= ?cvc_7 bv1[1]) (= ?cvc_7 bv0[1])) (if_then_else (if_then_else $cvc_6 (not $cvc_8) $cvc_8) (= ?cvc_9 bv1[1]) (= ?cvc_9 bv0[1])))) (and (= (extract[1:0] res) bv2[2]) (= (extract[1:0] c) bv1[2])))))))))))))) 18) 19