blob: a855f6787696858385ceed10e617da0c6716398b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_BV)
(declare-fun x1 () (_ BitVec 64))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 16))
(declare-fun x4 () (_ BitVec 8))
(declare-fun x5 () (_ BitVec 4))
(declare-fun x6 () (_ BitVec 2))
(declare-fun x7 () (_ BitVec 1))
(assert (= x1 (concat x2 x2)))
(assert (= x2 (concat x3 x3)))
(assert (= x3 (concat x4 x4)))
(assert (= x4 (concat x5 x5)))
(assert (= x5 (concat x6 x6)))
(assert (= x6 (concat x7 x7)))
(check-sat-assuming ( (not (= ((_ extract 0 0) x1) x7)) ))
|
