This is the list of verified benchmarks: - [x] `001_average` - [x] `002_fib` - [x] `003_gcd`. - [x] `004_matrix` - [x] `006_queens`. - [x] `007_regex`. - [ ] `008_scc`. (3 x `unsafe`) - [x] `009_lz77`. - [x] `010_sort`. _(doesn't verify deep property that returned array is sorted version of original)_ - [x] `011_codejam` - [ ] `012_cyclic`. (1 x `unsafe`) - [ ] `013_btree`. _(currently doesn't compile)_ - [x] `014_lights` - [ ] `015_cashtill` (3 x `unsafe`) - [ ] `016_date`. (1 x `unsafe`) - [x] `017_math`. - [ ] `018_heap`. (2 x `unsafe`, 1 x `assume`) _(big challenge with _preservation property_ as this requires a witness)_. - [x] `022_cars` - [x] `023_microwave` - [ ] `024_bits`. (1 x `unsafe`, some `assume`) - [x] `025_tries`. - [ ] `026_reverse`. (1 x `unsafe`, some `assume`) - [ ] `027_c_string`. (1 x `unsafe`, some `assume`) - [x] `028_flag`. _(but doesn't include deep property that result is permutation)_ - [ ] `029_bipmatch` - [x] `030_fractions` - [ ] `032_arrlist`. (1 x `assume`) - [x] `033_bank` - [ ] `102_conway` (3 x 'unsafe') - [ ] `104_tictactoe` (does not compile) - [ ] `107_minesweeper` (does not compile)
This is the list of verified benchmarks:
001_average002_fib003_gcd.004_matrix006_queens.007_regex.008_scc. (3 xunsafe)009_lz77.010_sort. (doesn't verify deep property that returned array is sorted version of original)011_codejam012_cyclic. (1 xunsafe)013_btree. (currently doesn't compile)014_lights015_cashtill(3 xunsafe)016_date. (1 xunsafe)017_math.018_heap. (2 xunsafe, 1 xassume) (big challenge with preservation property as this requires a witness).022_cars023_microwave024_bits. (1 xunsafe, someassume)025_tries.026_reverse. (1 xunsafe, someassume)027_c_string. (1 xunsafe, someassume)028_flag. (but doesn't include deep property that result is permutation)029_bipmatch030_fractions032_arrlist. (1 xassume)033_bank102_conway(3 x 'unsafe')104_tictactoe(does not compile)107_minesweeper(does not compile)