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:

• 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],

• 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:

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

[alex28sh]

• Final-Project-Dafny_tmp_tmpmcywuqox_Attempts_Merge_Sort.py
• HumanEval_intersperse.py
• HumanEval_largest_prime_factor.py
• 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