Commit 87024671 authored by Alain Mebsout's avatar Alain Mebsout

Importing snapshot 2015-06-01

parents
Pipeline #15 skipped

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun p () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (= ((_ sign_extend 24) (_ bv72 8)) ((_ sign_extend 24) (select p (_ bv0 32))))))
(assert (not (= ((_ sign_extend 24) (_ bv76 8)) ((_ sign_extend 24) (select p (_ bv0 32))))))
(assert (not (= ((_ sign_extend 24) (_ bv80 8)) ((_ sign_extend 24) (select p (_ bv0 32))))))
(assert (= ((_ sign_extend 24) (_ bv82 8)) ((_ sign_extend 24) (select p (_ bv0 32)))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((?v_0 (concat (concat (concat (concat ((_ extract 5 0) (select a (_ bv3 32))) (select a (_ bv2 32))) (select a (_ bv1 32))) (select a (_ bv0 32))) (_ bv0 2)))) (and (bvule (_ bv0 32) ?v_0) (bvule ?v_0 (_ bv3 32)))))
(check-sat)
(exit)
This source diff could not be displayed because it is too large. You can view the blob instead.
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((?v_0 (concat (concat (concat (concat ((_ extract 5 0) (select a (_ bv3 32))) (select a (_ bv2 32))) (select a (_ bv1 32))) (select a (_ bv0 32))) (_ bv0 2)))) (not (and (bvule (_ bv0 32) ?v_0) (bvule ?v_0 (_ bv3 32))))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (bvslt ((_ sign_extend 24) (select a (_ bv1 32))) ((_ sign_extend 24) (select a (_ bv0 32)))))
(assert (let ((?v_0 (store (store a (_ bv1 32) (select a (_ bv0 32))) (_ bv0 32) ((_ extract 7 0) ((_ sign_extend 24) (select a (_ bv1 32))))))) (not (bvslt ((_ sign_extend 24) (select ?v_0 (_ bv2 32))) ((_ sign_extend 24) (select ?v_0 (_ bv1 32)))))))
(assert (let ((?v_0 (store (store a (_ bv1 32) (select a (_ bv0 32))) (_ bv0 32) ((_ extract 7 0) ((_ sign_extend 24) (select a (_ bv1 32))))))) (bvslt ((_ sign_extend 24) (select ?v_0 (_ bv3 32))) ((_ sign_extend 24) (select ?v_0 (_ bv2 32))))))
(assert (let ((?v_0 (store (store a (_ bv1 32) (select a (_ bv0 32))) (_ bv0 32) ((_ extract 7 0) ((_ sign_extend 24) (select a (_ bv1 32))))))) (not (bvslt ((_ sign_extend 24) (select ?v_0 (_ bv3 32))) ((_ sign_extend 24) (select (store ?v_0 (_ bv3 32) (select ?v_0 (_ bv2 32))) (_ bv1 32)))))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun utf8 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (bvslt (concat (_ bv0 24) ((_ extract 7 0) (select utf8 (_ bv0 32)))) (_ bv128 32))))
(assert (not (bvslt (concat (_ bv0 24) ((_ extract 7 0) (select utf8 (_ bv0 32)))) (_ bv194 32))))
(assert (bvslt (concat (_ bv0 24) ((_ extract 7 0) (select utf8 (_ bv0 32)))) (_ bv224 32)))
(assert (not (= (bvand ((_ sign_extend 24) (select utf8 (_ bv1 32))) (_ bv192 32)) (_ bv128 32))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun i () (_ BitVec 32))
(declare-fun buf () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (and (bvule (_ bv0 32) i) (bvule i (_ bv3 32)))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (bvslt ((_ sign_extend 24) (select a (_ bv1 32))) ((_ sign_extend 24) (select a (_ bv0 32))))))
(assert (bvslt ((_ sign_extend 24) (select a (_ bv2 32))) ((_ sign_extend 24) (select a (_ bv1 32)))))
(assert (not (bvslt ((_ sign_extend 24) (select a (_ bv2 32))) ((_ sign_extend 24) (select (store a (_ bv2 32) (select a (_ bv1 32))) (_ bv0 32))))))
(assert (let ((?v_0 (store (store a (_ bv2 32) (select a (_ bv1 32))) (_ bv1 32) ((_ extract 7 0) ((_ sign_extend 24) (select a (_ bv2 32))))))) (not (bvslt ((_ sign_extend 24) (select ?v_0 (_ bv3 32))) ((_ sign_extend 24) (select ?v_0 (_ bv2 32)))))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun p () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (bvsle (_ bv48 32) (concat (_ bv0 24) (select p (_ bv0 32)))))
(assert (not (bvsle (concat (_ bv0 24) (select p (_ bv0 32))) (_ bv57 32))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun i () (_ BitVec 32))
(declare-fun buf () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (and (bvule (_ bv0 32) i) (bvule i (_ bv3 32))))
(assert (not (= (select buf i) (_ bv0 8))))
(check-sat)
(exit)
(set-logic QF_ABV)
(set-info :source |
Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using
CVC3.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun i () (_ BitVec 32))
(declare-fun buf () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (bvslt i (_ bv0 32))))
(assert (not (bvslt (_ bv4 32) i)))