(define a 1u32)
(define b 2u64)
(define c 1.0f32)
(define d 2.0f64)
(move-to-flash a b c d)
(check (and (= a 1)
(= a 1)
(= c 1.0)
(= d 2.0)))