Tracking issue for benchmark syncronization

[WeetHet]

The goal of this issue is to track the examples present in NaginiBench that are not yet verified in RustBench

There are currently four examples which I wasn't able to verify:

• [x] Barrier: replacing ==> with an equality causes the example to fail to verify

  
  13: result ==> forall|k: int, l: int| 0 <= k <= p && p < l < arr.len() ==> arr[k] < arr[l]

21: forall|k: int| 0 <= k < i ==> arr[max as int] >= arr[k],

- [x] `Recursive binary search`: fails due to not being able to verify termination
- [ ] `Mcontaied` fails due to the postcondition not being satisfied (maybe a bug in my code?)
- [ ] `Maximum segment sum`: I don't know how to write a spec sum function (asked in Zulip), integer overflows are possible (not that hard to fix probably)

[alex28sh]

Also:

• [x] dafny-language-server_tmp_tmpkir0kenl_Test_vstte2012_Two-Way-Sort
• [x] dafny-synthesis_task_id_161
• [x] dafny-synthesis_task_id_3
• [x] dafny-synthesis_task_id_401
• [x] dafny-synthesis_task_id_572
• [x] dafny-synthesis_task_id_610
• [x] dafny-synthesis_task_id_760
• [x] dafny-synthesis_task_id_793
• [x] dafny-synthesis_task_id_95

[alex28sh]

• [ ] Final-Project-Dafny_tmp_tmpmcywuqox_Attempts_Merge_Sort.py
• [x] HumanEval_intersperse.py
• [ ] HumanEval_largest_prime_factor.py
• [x] HumanEval_rolling_max.py
• [ ] dafny-language-server_tmp_tmpkir0kenl_Test_dafny1_MatrixFun.py
• [ ] verified-using-dafny_tmp_tmp7jatpjyn_longestZero.py
• [ ] summer-school-2020_tmp_tmpn8nf7zf0_chapter02_solutions_exercise03_solution.py