summaryrefslogtreecommitdiff
path: root/test/regress/regress0/aufbv/diseqprop.01.smt
blob: 4b31304759840b1e012bee74927da3d80a09a1ff (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

(benchmark B_
  :status unsat
  :logic QF_AUFBV
  
  :extrafuns ((x BitVec[32]))
  :extrafuns ((y BitVec[32]))
  :extrafuns ((a Array[32:8]))
  
  :assumption (not (= (store a x bv0[8]) (store a x (extract[7:0] y))))
  :assumption (= y bv0[32])

  :formula true
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback