(check (= 3u64 (+ 1u64 2u64)))