blob: 6bf931bb5cc594c2b49a5403df3b6d072a2fb963 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; COMMAND-LINE: --decision=justification
; EXPECT: unsat
(benchmark bitvec5.smt
:source {
Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite.
Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB
format by Clark Barrett using CVC3.
}
:status unsat
:difficulty { 0 }
:category { crafted }
:logic QF_BV
:extrafuns ((a BitVec[32]))
:extrafuns ((b BitVec[32]))
:extrafuns ((c BitVec[32]))
:extrafuns ((d BitVec[32]))
:extrafuns ((e BitVec[32]))
:formula
(not (and (implies (and (and (= (extract[31:0] a) (extract[31:0] b)) (= (extract[31:16] a) (extract[15:0] c))) (= (extract[31:8] b) (extract[23:0] d))) (= (extract[11:8] c) (extract[19:16] d))) (implies (= (extract[30:0] e) (extract[31:1] e)) (= (extract[0:0] e) (extract[31:31] e)))))
)
|
