Skip to content
GitLab
Commit c00a972e authored by Clark Barrett's avatar Clark Barrett
Browse files

Squashed commit of the following: 

commit 7552ddac
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 17:58:55 2017 +0200

    Fixing README.md

commit 9e7dc375
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 16:53:48 2017 +0200

    Fixing README.md

commit 5c94acf2
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Thu May 25 23:12:08 2017 +0200

    To version 2.6

commit 5ff7f3f8
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon May 22 15:39:57 2017 +0200

    2.0 to 2.5, CRLF to LF

commit ac95d970
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed May 3 18:20:58 2017 +0200

    Fixing README.md

commit 8471f0fe
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Thu Apr 20 10:08:37 2017 +0200

    Fixing README.md

commit 62a96b88
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed Mar 29 13:45:25 2017 +0200

    Fixing README.md

commit d9a0c82a
Author: Tjark Weber <tjark.weber@gmx.de>
Date:   Thu Mar 16 10:31:25 2017 +0100

    Remove duplicate benchmarks
parent cce2fd0d
Hide whitespace changes
Inline Side-by-side
ecc/com.galois.ecc.P384ECC64.ec_full_add.short.smt2 deleted 100644 → 0
View file @ cce2fd0d
(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)
ecc/com.galois.ecc.P384ECC64.ec_full_add1.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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))
......
ecc/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x220 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x260 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x241 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_full_add5.short.smt2 deleted 100644 → 0
View file @ cce2fd0d
(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)
ecc/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x55 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x55 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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 x55 () (_ BitVec 1))
......
ecc/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2
View file @ c00a972e
(set-info :smt-lib-version 2.6)
(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|)