Commit a263f213 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Move benchmarks from pending repository.

parent c35d070b
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)
; This file was generated with the help of KLEE
(set-info :source |
Generated by: Alexandre Gonzalvez
Generated on: 2019-02-28
Generator: KLEE
Target solver: Boolector Z3 STP
Benchmarks arising from a generator of opaque expressions
These expressions are used to protect some constants against
reverse-engineering, but their robustness can be compromised by
SMT-solvers
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
; Number of instructions: 475
; Time expected : less than 1 minute
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat (select x (_ bv3 32) ) (concat (select x (_ bv2 32) ) (concat (select x (_ bv1 32) ) (select x (_ bv0 32) ) ) ) ) ) ) (let ( (?B2 (bvmul ?B1 ?B1 ) ) ) (let ( (?B3 (bvmul (_ bv715827882 32) ?B2 ) ) ) (let ( (?B4 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B3 ) (_ bv2 32) ) ) ?B3 ) ) ) (let ( (?B5 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B4 ) (_ bv2 32) ) ) ?B4 ) ) ) (let ( (?B6 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B5 ) (_ bv2 32) ) ) ?B5 ) ) ) (let ( (?B7 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B6 ) (_ bv2 32) ) ) ?B6 ) ) ) (let ( (?B8 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B7 ) (_ bv2 32) ) ) ?B7 ) ) ) (let ( (?B9 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B8 ) (_ bv2 32) ) ) ?B8 ) ) ) (let ( (?B10 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B9 ) (_ bv2 32) ) ) ?B9 ) ) ) (let ( (?B11 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B10 ) (_ bv2 32) ) ) ?B10 ) ) ) (let ( (?B12 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B11 ) (_ bv2 32) ) ) ?B11 ) ) ) (let ( (?B13 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B12 ) (_ bv2 32) ) ) ?B12 ) ) ) (let ( (?B14 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B13 ) (_ bv2 32) ) ) ?B13 ) ) ) (let ( (?B15 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B14 ) (_ bv2 32) ) ) ?B14 ) ) ) (let ( (?B16 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B15 ) (_ bv2 32) ) ) ?B15 ) ) ) (let ( (?B17 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B16 ) (_ bv2 32) ) ) ?B16 ) ) ) (and (= (_ bv3657258328 32) (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B17 ) (_ bv2 32) ) ) ?B17 ) ) (= (_ bv1 32) (concat (select model_version (_ bv3 32) ) (concat (select model_version (_ bv2 32) ) (concat (select model_version (_ bv1 32) ) (select model_version (_ bv0 32) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)
; This file conforms to SMTLIBv2 and was generated by KLEE
(set-info :source |
Generated by: Alexandre Gonzalvez
Generated on: 2019-02-28
Generator: KLEE
Target solver: Boolector Z3 STP
Benchmarks arising from a generator of opaque expressions
These expressions are used to protect some constants against
reverse-engineering, but their robustness can be compromised by
SMT-solvers
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
; Number of instructions: 627
; Time expected : less than 1 minute
; Array declarations
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
; Constraints
; Constraints and QueryExpr
(assert
(let
(
(?B1
(concat
(select
x
(_ bv3 32)
)
(concat
(select
x
(_ bv2 32)
)
(concat
(select
x
(_ bv1 32)
)
(select
x
(_ bv0 32)
)
)
)
)
)
)
(let
(
(?B2
(bvmul
(_ bv715827882 32)
?B1
)
)
)
(let
(
(?B3
(bvadd
?B2
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B2
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B4
(bvadd
?B3
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B3
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B5
(bvadd
?B4
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B4
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B6
(bvadd
?B5
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B5
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B7
(bvadd
?B6
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B6
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B8
(bvadd
?B7
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B7
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B9
(bvadd
?B8
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B8
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B10
(bvadd
?B9
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B9
)
(_ bv2 32)
)
)
)
)
)
(and
(=
(_ bv1506744832 32)
(bvadd
?B10
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B10
)
(_ bv2 32)
)
)
)
)
(=
(_ bv1 32)
(concat
(select
model_version
(_ bv3 32)
)
(concat
(select
model_version
(_ bv2 32)
)
(concat
(select
model_version
(_ bv1 32)
)
(select
model_version
(_ bv0 32)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(check-sat)
(exit)
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment