blob: be52810e0d4a477a530e384077123c5014620fb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(set-option :produce-models true)
(set-logic QF_BV)
(set-info :status sat)
(set-info :source |
Patrice Godefroid, SAGE (systematic dynamic test generation)
For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun z () (_ BitVec 4))
(assert (or
(= x (bvmul x y))
(and (= x y)
(not (= ((_ extract 2 2) x) ((_ extract 2 2) z))))
))
(check-sat)
(exit)
|
