Commit a0e7648b authored by Alain Mebsout's avatar Alain Mebsout
Browse files

Importing snapshot 2015-06-01

parents
Pipeline #14 skipped
(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x87 () (_ BitVec 1))
(declare-fun x85 () (_ BitVec 1))
(declare-fun x83 () (_ BitVec 1))
(declare-fun x81 () (_ BitVec 1))
(declare-fun x79 () (_ BitVec 1))
(declare-fun x78 () (_ BitVec 1))
(declare-fun x77 () (_ BitVec 384))
(declare-fun x76 () (_ BitVec 384))
(declare-fun x75 () (_ BitVec 384))
(declare-fun x74 () (_ BitVec 384))
(declare-fun x73 () (_ BitVec 384))
(declare-fun x72 () (_ BitVec 384))
(declare-fun x71 () (_ BitVec 384))
(declare-fun x70 () (_ BitVec 384))
(declare-fun x69 () (_ BitVec 384))
(declare-fun x68 () (_ BitVec 384))
(declare-fun x67 () (_ BitVec 384))
(declare-fun x66 () (_ BitVec 384))
(declare-fun x65 () (_ BitVec 384))
(declare-fun x64 () (_ BitVec 384))
(declare-fun x63 () (_ BitVec 384))
(declare-fun x62 () (_ BitVec 1))
(declare-fun x60 () (_ BitVec 1))
(declare-fun x59 () (_ BitVec 1))
(declare-fun x58 () (_ BitVec 384))
(declare-fun x57 () (_ BitVec 384))
(declare-fun x56 () (_ BitVec 384))
(declare-fun x55 ((_ BitVec 384) (_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x54 () (_ BitVec 384))
(declare-fun x53 () (_ BitVec 384))
(declare-fun x52 () (_ BitVec 384))
(declare-fun x51 () (_ BitVec 384))
(declare-fun x50 () (_ BitVec 384))
(declare-fun x49 () (_ BitVec 384))
(declare-fun x48 () (_ BitVec 384))
(declare-fun x47 () (_ BitVec 384))
(declare-fun x46 () (_ BitVec 384))
(declare-fun x45 () (_ BitVec 384))
(declare-fun x44 () (_ BitVec 384))
(declare-fun x43 () (_ BitVec 384))
(declare-fun x41 () (_ BitVec 1))
(declare-fun x40 () (_ BitVec 1))
(declare-fun x39 () (_ BitVec 384))
(declare-fun x38 () (_ BitVec 384))
(declare-fun x37 () (_ BitVec 1))
(declare-fun x35 () (_ BitVec 1))
(declare-fun x34 () (_ BitVec 1))
(declare-fun x33 () (_ BitVec 384))
(declare-fun x32 ((_ BitVec 384) (_ BitVec 384) (_ BitVec 384) (_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x31 () (_ BitVec 384))
(declare-fun x30 ((_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x29 () (_ BitVec 384))
(declare-fun x28 () (_ BitVec 384))
(declare-fun x27 () (_ BitVec 384))
(declare-fun x26 () (_ BitVec 384))
(declare-fun x25 () (_ BitVec 384))
(declare-fun x24 () (_ BitVec 384))
(declare-fun x23 () (_ BitVec 384))
(declare-fun x22 () (_ BitVec 384))
(declare-fun x20 () (_ BitVec 1))
(declare-fun x19 () (_ BitVec 1))
(declare-fun x18 () (_ BitVec 384))
(declare-fun x17 () (_ BitVec 384))
(declare-fun x16 () (_ BitVec 1))
(declare-fun x15 () (_ BitVec 1))
(declare-fun x14 () (_ BitVec 384))
(declare-fun x13 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x12 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x11 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x10 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x9 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x8 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x7 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x6 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x5 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x4 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x3 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x2 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x1 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x0 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun p88 () Bool)
(declare-fun p86 () Bool)
(declare-fun p84 () Bool)
(declare-fun p82 () Bool)
(declare-fun p80 () Bool)
(declare-fun p61 () Bool)
(declare-fun p42 () Bool)
(declare-fun p36 () Bool)
(declare-fun p21 () Bool)
(assert (= p88 (or (= x14 (_ bv0 384)) p86)))
(assert (= x87 (bvor x16 x85)))
(assert (= p86 (and p36 p84)))
(assert (= x85 (bvand x35 x83)))
(assert (= p84 (or (= x18 (_ bv0 384)) p82)))
(assert (= x83 (bvor x37 x81)))
(assert (= p82 (and p61 p80)))
(assert (= x81 (bvand x60 x79)))
(assert (= p80 (or (bvule x38 x39) (= x63 x77))))
(assert (= x79 (bvor x62 x78)))
(assert (= x78 (ite (= x63 x77) (_ bv1 1) (_ bv0 1))))
(assert (= x77 (x32 x64 x65 x66 x70 x76)))
(assert (= x76 (x30 x71 x75)))
(assert (= x75 (x55 x72 x73 x74)))
(assert (= x74 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x73 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= x72 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x71 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x70 (bvlshr x69 (_ bv1 384))))
(assert (= x69 (bvsub x67 x68)))
(assert (= x68 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x67 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x66 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x65 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x64 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x63 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= x62 (ite (bvule x38 x39) (_ bv1 1) (_ bv0 1))))
(assert (= p61 (or p42 (= x43 x58))))
(assert (= x60 (bvor x41 x59)))
(assert (= x59 (ite (= x43 x58) (_ bv1 1) (_ bv0 1))))
(assert (= x58 (x32 x44 x45 x46 x50 x57)))
(assert (= x57 (x30 x51 x56)))
(assert (= x56 (x55 x52 x53 x54)))
(assert (= x54 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= x53 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x52 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x51 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x50 (bvlshr x49 (_ bv1 384))))
(assert (= x49 (bvsub x47 x48)))
(assert (= x48 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x47 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x46 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= x45 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x44 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x43 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= p42 (not (bvule x38 x39))))
(assert (= x41 (bvnot x40)))
(assert (= x40 (ite (bvule x38 x39) (_ bv1 1) (_ bv0 1))))
(assert (= x39 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x38 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x37 (ite (= x18 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= p36 (or p21 (= x22 x33))))
(assert (= x35 (bvor x20 x34)))
(assert (= x34 (ite (= x22 x33) (_ bv1 1) (_ bv0 1))))
(assert (= x33 (x32 x23 x24 x25 x27 x31)))
(assert (= x31 (x30 x28 x29)))
(assert (= x29 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x28 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x27 (bvlshr x26 (_ bv1 384))))
(assert (= x26 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x25 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= x24 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x23 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x22 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= p21 (not (= x18 (_ bv0 384)))))
(assert (= x20 (bvnot x19)))
(assert (= x19 (ite (= x18 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x18 (bvand x17 (_ bv1 384))))
(assert (= x17 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x16 (ite (= x14 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x15 (ite (= x14 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x14 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert true)
(assert (= (select x13 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv12 4)) (_ bv0 32)))
(assert (not (=> (= x14 (_ bv0 384)) p88)))
(check-sat)
(exit)
(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x71 () (_ BitVec 1))
(declare-fun x69 () (_ BitVec 1))
(declare-fun x67 () (_ BitVec 1))
(declare-fun x65 () (_ BitVec 1))
(declare-fun x64 () (_ BitVec 1))
(declare-fun x63 () (_ BitVec 1))
(declare-fun x61 () (_ BitVec 1))
(declare-fun x59 () (_ BitVec 1))
(declare-fun x57 () (_ BitVec 1))
(declare-fun x55 () (_ BitVec 1))
(declare-fun x54 () (_ BitVec 1))
(declare-fun x52 () (_ BitVec 1))
(declare-fun x51 () (_ BitVec 1))
(declare-fun x50 () (_ BitVec 384))
(declare-fun x49 () (_ BitVec 384))
(declare-fun x48 () (_ BitVec 384))
(declare-fun x47 () (_ BitVec 384))
(declare-fun x46 () (_ BitVec 384))
(declare-fun x45 () (_ BitVec 384))
(declare-fun x44 () (_ BitVec 384))
(declare-fun x42 () (_ BitVec 1))
(declare-fun x41 () (_ BitVec 1))
(declare-fun x39 () (_ BitVec 1))
(declare-fun x37 () (_ BitVec 1))
(declare-fun x36 () (_ BitVec 1))
(declare-fun x35 () (_ BitVec 384))
(declare-fun x33 () (_ BitVec 1))
(declare-fun x32 () (_ BitVec 1))
(declare-fun x31 () (_ BitVec 384))
(declare-fun x30 ((_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x29 () (_ BitVec 384))
(declare-fun x28 ((_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x27 () (_ BitVec 384))
(declare-fun x26 ((_ BitVec 384)) (_ BitVec 384))
(declare-fun x25 () (_ BitVec 384))
(declare-fun x24 () (_ BitVec 384))
(declare-fun x23 () (_ BitVec 384))
(declare-fun x22 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x21 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x20 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x19 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x18 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x17 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x16 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x15 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x14 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x13 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x12 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x11 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x10 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x9 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x8 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x7 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x6 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x5 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x4 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x3 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x2 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x1 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x0 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun p72 () Bool)
(declare-fun p70 () Bool)
(declare-fun p68 () Bool)
(declare-fun p66 () Bool)
(declare-fun p62 () Bool)
(declare-fun p60 () Bool)
(declare-fun p58 () Bool)
(declare-fun p56 () Bool)
(declare-fun p53 () Bool)
(declare-fun p43 () Bool)
(declare-fun p40 () Bool)
(declare-fun p38 () Bool)
(declare-fun p34 () Bool)
(assert (= p72 (or p62 p70)))
(assert (= x71 (bvor x61 x69)))
(assert (= p70 (and p66 p68)))
(assert (= x69 (bvand x65 x67)))
(assert (= p68 (not (= x35 (_ bv0 384)))))
(assert (= x67 (bvnot x36)))
(assert (= p66 (and (= x50 (_ bv0 384)) (= x31 (_ bv0 384)))))
(assert (= x65 (bvand x63 x64)))
(assert (= x64 (ite (= x31 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x63 (ite (= x50 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= p62 (or p43 p60)))
(assert (= x61 (bvor x42 x59)))
(assert (= p60 (and p56 p58)))
(assert (= x59 (bvand x55 x57)))
(assert (= p58 (not (= x35 (_ bv0 384)))))
(assert (= x57 (bvnot x36)))
(assert (= p56 (and p53 (= x31 (_ bv0 384)))))
(assert (= x55 (bvand x52 x54)))
(assert (= x54 (ite (= x31 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= p53 (not (= x50 (_ bv0 384)))))
(assert (= x52 (bvnot x51)))
(assert (= x51 (ite (= x50 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x50 (x30 x44 x49)))
(assert (= x49 (x28 x45 x48)))
(assert (= x48 (x28 x46 x47)))
(assert (= x47 (x26 x25)))
(assert (= x46 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x45 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x44 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= p43 (or p40 (= x35 (_ bv0 384)))))
(assert (= x42 (bvor x39 x41)))
(assert (= x41 (ite (= x35 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= p40 (and p34 p38)))
(assert (= x39 (bvand x33 x37)))
(assert (= p38 (not (= x35 (_ bv0 384)))))
(assert (= x37 (bvnot x36)))
(assert (= x36 (ite (= x35 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x35 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= p34 (not (= x31 (_ bv0 384)))))
(assert (= x33 (bvnot x32)))
(assert (= x32 (ite (= x31 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x31 (x30 x23 x29)))
(assert (= x29 (x28 x24 x27)))
(assert (= x27 (x26 x25)))
(assert (= x25 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x24 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x23 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert true)
(assert (= (select x22 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x22 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x21 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x19 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x19 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x18 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x15 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x14 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x11 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x10 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x8 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv12 4)) (_ bv0 32)))
(assert (not (=> p72 true)))
(check-sat)
(exit)
This diff is collapsed.
<
(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x83 () (_ BitVec 1))
(declare-fun x81 () (_ BitVec 1))
(declare-fun x80 () (_ BitVec 1))
(declare-fun x79 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x78 () (_ BitVec 32))
(declare-fun x77 () (_ BitVec 64))
(declare-fun x76 () (_ BitVec 64))
(declare-fun x75 () (_ BitVec 64))
(declare-fun x74 () (_ BitVec 32))
(declare-fun x73 () (_ BitVec 64))
(declare-fun x71 () (_ BitVec 1))
(declare-fun x69 () (_ BitVec 1))
(declare-fun x68 () (_ BitVec 1))
(declare-fun x67 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x66 () (_ BitVec 768))
(declare-fun x65 () (_ BitVec 832))
(declare-fun x64 ((_ BitVec 32) (_ BitVec 768) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ BitVec 64)) (_ BitVec 832))
(declare-fun x63 () (_ BitVec 768))
(declare-fun x62 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x61 () (_ BitVec 32))
(declare-fun x60 () (_ BitVec 64))
(declare-fun x59 () (_ BitVec 64))
(declare-fun x58 () (_ BitVec 64))
(declare-fun x57 () (_ BitVec 64))
(declare-fun x56 () (_ BitVec 64))
(declare-fun x55 () (_ BitVec 64))
(declare-fun x54 () (_ BitVec 64))
(declare-fun x52 () (_ BitVec 1))
(declare-fun x50 () (_ BitVec 1))
(declare-fun x49 () (_ BitVec 1))
(declare-fun x47 () (_ BitVec 1))
(declare-fun x45 () (_ BitVec 1))
(declare-fun x43 () (_ BitVec 1))
(declare-fun x42 () (_ BitVec 1))
(declare-fun x40 () (_ BitVec 1))
(declare-fun x39 () (_ BitVec 1))
(declare-fun x37 () (_ BitVec 1))
(declare-fun x36 () (_ BitVec 1))
(declare-fun x34 () (_ BitVec 1))
(declare-fun x32 () (_ BitVec 1))
(declare-fun x31 () (_ BitVec 1))
(declare-fun x29 () (_ BitVec 1))
(declare-fun x28 () (_ BitVec 1))
(declare-fun x26 () (_ BitVec 1))
(declare-fun x25 () (_ BitVec 1))
(declare-fun x23 () (_ BitVec 1))
(declare-fun x21 () (_ BitVec 1))
(declare-fun x20 () (_ BitVec 1))
(declare-fun x18 () (_ BitVec 1))
(declare-fun x17 () (_ BitVec 1))
(declare-fun x15 () (_ BitVec 1))
(declare-fun x13 () (_ BitVec 1))
(declare-fun x12 () (_ BitVec 1))
(declare-fun x10 () (_ BitVec 1))
(declare-fun x8 () (_ BitVec 1))
(declare-fun x7 () (_ BitVec 1))
(declare-fun x6 () (_ BitVec 1))
(declare-fun x5 () (_ BitVec 32))
(declare-fun x4 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x0 () (_ BitVec 64))
(declare-fun p84 () Bool)
(declare-fun p82 () Bool)
(declare-fun p72 () Bool)
(declare-fun p70 () Bool)
(declare-fun p53 () Bool)
(declare-fun p51 () Bool)
(declare-fun p48 () Bool)
(declare-fun p46 () Bool)
(declare-fun p44 () Bool)
(declare-fun p41 () Bool)
(declare-fun p38 () Bool)
(declare-fun p35 () Bool)
(declare-fun p33 () Bool)
(declare-fun p30 () Bool)
(declare-fun p27 () Bool)
(declare-fun p24 () Bool)
(declare-fun p22 () Bool)
(declare-fun p19 () Bool)
(declare-fun p16 () Bool)
(declare-fun p14 () Bool)
(declare-fun p11 () Bool)
(declare-fun p9 () Bool)
(assert (= p84 (and p70 p82)))
(assert (= x83 (bvand x69 x81)))
(assert (= p82 (or p72 (= x79 x67))))
(assert (= x81 (bvor x71 x80)))
(assert (= x80 (ite (= x79 x67) (_ bv1 1) (_ bv0 1))))
(assert (= x79 (store x4 ((_ extract 4 0) x3) x78)))
(assert (= (select x79 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv24 5)) (_ bv0 32)))
(assert (= x78 ((_ extract 31 0) x77)))
(assert (= x77 (bvadd x73 x76)))