blob: 7270afa68f83682525c3aff4f69de7219a4625ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(set-logic QF_BV)
(declare-fun a () (_ BitVec 4))
(declare-fun b () (_ BitVec 4))
(declare-fun c () (_ BitVec 4))
(declare-fun d () (_ BitVec 4))
(assert (= #b0010 a))
(assert (= #b0110 b))
(assert (= #b1000 c))
(assert (= #b1100 d))
(assert
(not (= (bvmul a b) d)))
(check-sat)
(exit)
|