diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs
new file mode 100644
index 00000000000..a0465881401
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared.rs
@@ -0,0 +1,170 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
+//! An adaptation of the example from
+//! https://rosettacode.org/wiki/Binary_search#Rust
+//!
+//! The original example:
+//! ```rust
+//! use std::cmp::Ordering::*;
+//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
+//! {
+//!     let mut size = arr.len();
+//!     let mut base = 0;
+//!
+//!     while size > 0 {
+//!         size /= 2;
+//!         let mid = base + size;
+//!         base = match arr[mid].cmp(elem) {
+//!             Less    => mid,
+//!             Greater => base,
+//!             Equal   => return Some(mid)
+//!         };
+//!     }
+//!
+//!     None
+//! }
+//! ```
+//!
+//! Changes:
+//!
+//! +   Wrapped built-in types and functions.
+//! +   Replaced a slice with a reference into a vector.
+//! +   Change the loop into the supported shape.
+//! +   Remove the return statement.
+//!
+//! Verified properties:
+//!
+//! +   Absence of panics.
+//! +   Absence of overflows.
+//!
+//! The original example contains a bug, which can be showed by using
+//! the following counter-example:
+//!
+//! ```rust
+//! fn main() {
+//!     let v = vec![0, 1, 2, 3, 4, 5, 6];
+//!     println!("{:?}", binary_search(&v, &6));
+//! }
+//! ```
+//!
+//! This program should print `Some(6)`, but it prints None. The fixed
+//! version would be:
+//!
+//! ```rust
+//! use std::cmp::Ordering::*;
+//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
+//! {
+//!     let mut size = arr.len();
+//!     let mut base = 0;
+//!
+//!     while size > 0 {
+//!         let half = size / 2;
+//!         let mid = base + half;
+//!         base = match arr[mid].cmp(elem) {
+//!             Less    => mid,
+//!             Greater => base,
+//!             Equal   => return Some(mid)
+//!         };
+//!         size -= half;
+//!     }
+//!
+//!     None
+//! }
+//! ```
+//!
+//! This file contains a verified version of it.
+
+use prusti_contracts::*;
+
+pub struct VecWrapper<T>{
+    v: Vec<T>
+}
+
+impl<T> VecWrapper<T> {
+
+    #[trusted]
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.v.len()
+    }
+
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    pub fn index(&self, index: usize) -> &T {
+        &self.v[index]
+    }
+}
+
+pub enum UsizeOption {
+    Some(usize),
+    None,
+}
+
+impl UsizeOption {
+    #[pure]
+    pub fn is_some(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => true,
+            UsizeOption::None => false,
+        }
+    }
+    #[pure]
+    pub fn is_none(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => false,
+            UsizeOption::None => true,
+        }
+    }
+}
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+use self::Ordering::*;
+
+#[trusted]
+fn cmp<T>(_a: &T, _b: &T) -> Ordering {
+    unimplemented!();
+}
+
+fn binary_search<T: Ord>(arr: &VecWrapper<T>, elem: &T) -> UsizeOption {
+    let mut size = arr.len();
+    let mut base = 0;
+
+    let mut result = UsizeOption::None;
+    let mut continue_loop = size > 0;
+
+
+    while continue_loop {
+        body_invariant!(continue_loop == (size > 0 && result.is_none()));
+        body_invariant!(base + size <= arr.len());
+        let half = size / 2;
+        let mid = base + half;
+
+        let mid_element = arr.index(mid);
+        let cmp_result = cmp(mid_element, elem);
+        base = match cmp_result {
+            Less    => {
+                mid
+            },
+            Greater => {
+                base
+            },
+            // Equal
+            _   => {
+                result = UsizeOption::Some(mid);
+                base   // Just return anything because we are finished.
+            }
+        };
+
+        size -= half;
+        continue_loop = size > 0 && result.is_none();
+    }
+
+    result
+}
+
+fn main() {}
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs
new file mode 100644
index 00000000000..8916a3d83a1
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_fixed_termination.rs
@@ -0,0 +1,107 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
+//! A copy of `artefact_Binary_search_shared.rs` with fixed non-termination bug and manually
+//! encoded termination check.
+
+use prusti_contracts::*;
+
+pub struct VecWrapper<T>{
+    v: Vec<T>
+}
+
+impl<T> VecWrapper<T> {
+
+    #[trusted]
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.v.len()
+    }
+
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    pub fn index(&self, index: usize) -> &T {
+        &self.v[index]
+    }
+}
+
+pub enum UsizeOption {
+    Some(usize),
+    None,
+}
+
+impl UsizeOption {
+    #[pure]
+    pub fn is_some(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => true,
+            UsizeOption::None => false,
+        }
+    }
+    #[pure]
+    pub fn is_none(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => false,
+            UsizeOption::None => true,
+        }
+    }
+}
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+use self::Ordering::*;
+
+#[trusted]
+fn cmp<T>(_a: &T, _b: &T) -> Ordering {
+    unimplemented!();
+}
+
+fn binary_search<T: Ord>(arr: &VecWrapper<T>, elem: &T) -> UsizeOption {
+    let mut size = arr.len();
+    let mut base = 0;
+
+    let mut result = UsizeOption::None;
+    let mut continue_loop = size > 0;
+
+
+    while continue_loop {
+        body_invariant!(continue_loop == (size > 0 && result.is_none()));
+        body_invariant!(base + size <= arr.len());
+        let ghost_old_size = size;
+
+        let half = size / 2;
+        let mid = base + half;
+
+        let mid_element = arr.index(mid);
+        let cmp_result = cmp(mid_element, elem);
+        base = match cmp_result {
+            Less    => {
+                mid
+            },
+            Greater => {
+                base
+            },
+            // Equal
+            _   => {
+                result = UsizeOption::Some(mid);
+                base   // Just return anything because we are finished.
+            }
+        };
+
+        if half == 0 {
+            break;
+        }
+
+        size -= half;
+        continue_loop = size > 0 && result.is_none();
+
+        prusti_assert!(ghost_old_size >= 0 && ghost_old_size > size);   // Termination check.
+    }
+
+    result
+}
+
+fn main() {}
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_generic_functional.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_generic_functional.rs
new file mode 100644
index 00000000000..82f833cedfc
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_generic_functional.rs
@@ -0,0 +1,168 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
+//! A copy of `artefact_Binary_search_shared.rs` with fixed non-termination bug and manually
+//! encoded termination check.
+
+use prusti_contracts::*;
+
+pub struct VecWrapper<T>{
+    v: Vec<T>
+}
+
+impl<T> VecWrapper<T> {
+
+    #[trusted]
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.v.len()
+    }
+
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    #[ensures(result === self.lookup(index))]
+    pub fn index(&self, index: usize) -> &T {
+        &self.v[index]
+    }
+
+    #[pure]
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    pub fn lookup(&self, index: usize) -> &T {
+        &self.v[index]
+    }
+}
+
+pub enum MyOption<T> {
+    Some(T),
+    None,
+}
+
+impl<T> MyOption<T> {
+    #[pure]
+    pub fn is_some(&self) -> bool {
+        match self {
+            MyOption::Some(_) => true,
+            MyOption::None => false,
+        }
+    }
+    #[pure]
+    pub fn is_none(&self) -> bool {
+        match self {
+            MyOption::Some(_) => false,
+            MyOption::None => true,
+        }
+    }
+}
+
+#[derive(Clone, Copy)]
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+use self::Ordering::*;
+
+#[trusted]
+#[pure]
+#[ensures(matches!(result, Equal) == (a === b))]
+fn cmp<T: Ord>(a: &T, b: &T) -> Ordering {
+    match Ord::cmp(a, b) {
+        std::cmp::Ordering::Less => Less,
+        std::cmp::Ordering::Equal => Equal,
+        std::cmp::Ordering::Greater => Greater,
+    }
+}
+
+#[trusted]
+#[requires(cmp(bound, elem) === Less)]
+#[ensures(
+    forall(|a: &T|
+        matches!(cmp(a, bound), Less | Equal) ==>
+        cmp(a, elem) === Less,
+        triggers=[(cmp(a, elem),)])
+)]
+fn lemma_cmp_less_transitive<T: Ord>(bound: &T, elem: &T) {}
+
+#[trusted]
+#[requires(cmp(bound, elem) === Greater)]
+#[ensures(
+    forall(|a: &T|
+        matches!(cmp(bound, a), Less | Equal) ==>
+        cmp(a, elem) === Greater,
+        triggers=[(cmp(a, elem),)])
+)]
+fn lemma_cmp_greater_transitive<T: Ord>(bound: &T, elem: &T) {}
+
+#[requires(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
+             matches!(cmp(arr.lookup(k1), arr.lookup(k2)), Less | Equal)))]
+#[ensures(result.is_none() ==>
+            (forall(|k: usize| (0 <= k && k < arr.len()) ==> elem !== arr.lookup(k))))]
+#[ensures(match result {
+                MyOption::Some(index) => (
+                    0 <= index && index < arr.len() &&
+                    arr.lookup(index) === elem
+                ),
+                MyOption::None => true,
+            })]
+fn binary_search<T: Ord>(arr: &VecWrapper<T>, elem: &T) -> MyOption<usize> {
+    let mut size = arr.len();
+    let mut base = 0;
+
+    let mut result = MyOption::None;
+    let mut continue_loop = size > 0;
+
+
+    while continue_loop {
+        body_invariant!(continue_loop == (size > 0 && result.is_none()));
+        body_invariant!(base + size <= arr.len());
+        body_invariant!(forall(|k: usize| (0 <= k && k < base) ==>
+            cmp(arr.lookup(k), elem) === Less, triggers=[(arr.lookup(k),),]));
+        body_invariant!(result.is_none() ==>
+                (forall(|k: usize| (base + size <= k && k < arr.len()) ==>
+                        cmp(arr.lookup(k), elem) === Greater, triggers=[(arr.lookup(k),),])));
+        body_invariant!(match result {
+                    MyOption::Some(index) => (
+                        0 <= index && index < arr.len() &&
+                        arr.lookup(index) === elem
+                    ),
+                    MyOption::None => true,
+                });
+        let ghost_old_size = size;
+
+        let half = size / 2;
+        let mid = base + half;
+
+        let mid_element = arr.index(mid);
+        let cmp_result = cmp(mid_element, elem);
+        base = match cmp_result {
+            Less    => {
+                lemma_cmp_less_transitive(mid_element, elem);
+                mid
+            },
+            Greater => {
+                lemma_cmp_greater_transitive(mid_element, elem);
+                base
+            },
+            // Equal
+            _   => {
+                result = MyOption::Some(mid);
+                base   // Just return anything because we are finished.
+            }
+        };
+
+        if half == 0 {
+            break;
+        }
+
+        size -= half;
+        continue_loop = size > 0 && result.is_none();
+
+        prusti_assert!(ghost_old_size >= 0 && ghost_old_size > size);   // Termination check.
+    }
+
+    result
+}
+
+fn main() {}
+
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs
new file mode 100644
index 00000000000..65962859a4e
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised.rs
@@ -0,0 +1,212 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
+//! An adaptation of the example from
+//! https://rosettacode.org/wiki/Binary_search#Rust
+//!
+//! The original example:
+//! ```rust
+//! use std::cmp::Ordering::*;
+//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
+//! {
+//!     let mut size = arr.len();
+//!     let mut base = 0;
+//!
+//!     while size > 0 {
+//!         size /= 2;
+//!         let mid = base + size;
+//!         base = match arr[mid].cmp(elem) {
+//!             Less    => mid,
+//!             Greater => base,
+//!             Equal   => return Some(mid)
+//!         };
+//!     }
+//!
+//!     None
+//! }
+//! ```
+//!
+//! Changes:
+//!
+//! +   Wrapped built-in types and functions.
+//! +   Add additional functions for capturing functional specification.
+//! +   Replaced a slice with a reference into a vector.
+//! +   Changed the loop into the supported shape.
+//! +   Removed the return statement.
+//! +   Monomorphised types.
+//!
+//! Verified properties:
+//!
+//! +   Absence of panics.
+//! +   Absence of overflows.
+//! +   If the result is `None`, then the input vector did not contain the
+//!     element.
+//! +   If the result is `Some(index)` then the `arr[index] == elem`.
+//!
+//! The original example contains a bug, which can be showed by using
+//! the following counter-example:
+//!
+//! ```rust
+//! fn main() {
+//!     let v = vec![0, 1, 2, 3, 4, 5, 6];
+//!     println!("{:?}", binary_search(&v, &6));
+//! }
+//! ```
+//!
+//! This program should print `Some(6)`, but it prints None. The fixed
+//! version would be:
+//!
+//! ```rust
+//! use std::cmp::Ordering::*;
+//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
+//! {
+//!     let mut size = arr.len();
+//!     let mut base = 0;
+//!
+//!     while size > 0 {
+//!         let half = size / 2;
+//!         let mid = base + half;
+//!         base = match arr[mid].cmp(elem) {
+//!             Less    => mid,
+//!             Greater => base,
+//!             Equal   => return Some(mid)
+//!         };
+//!         size -= half;
+//!     }
+//!
+//!     None
+//! }
+//! ```
+//!
+//! This file contains a verified version of it.
+
+use prusti_contracts::*;
+
+pub struct VecWrapperI32{
+    v: Vec<i32>
+}
+
+impl VecWrapperI32 {
+    #[trusted]
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.v.len()
+    }
+
+    #[trusted]
+    #[pure]
+    #[requires(0 <= index && index < self.len())]
+    pub fn lookup(&self, index: usize) -> i32 {
+        self.v[index]
+    }
+
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    #[ensures(self.lookup(index) == *result)]
+    pub fn index(&self, index: usize) -> &i32 {
+        &self.v[index]
+    }
+}
+
+pub enum UsizeOption {
+    Some(usize),
+    None,
+}
+
+impl UsizeOption {
+    #[pure]
+    pub fn is_some(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => true,
+            UsizeOption::None => false,
+        }
+    }
+    #[pure]
+    pub fn is_none(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => false,
+            UsizeOption::None => true,
+        }
+    }
+}
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+use self::Ordering::*;
+
+#[ensures(match result {
+                Equal => *a == *b,
+                Less => *a < *b,
+                Greater => *a > *b,
+            })]
+fn cmp(a: &i32, b: &i32) -> Ordering {
+    if *a == *b { Equal }
+        else if *a < *b { Less }
+            else { Greater }
+}
+
+
+#[requires(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
+             arr.lookup(k1) <= arr.lookup(k2)))]
+#[ensures(result.is_none() ==>
+            (forall(|k: usize| (0 <= k && k < arr.len()) ==> *elem != arr.lookup(k))))]
+#[ensures(match result {
+                UsizeOption::Some(index) => (
+                    0 <= index && index < arr.len() &&
+                    arr.lookup(index) == *elem
+                ),
+                UsizeOption::None => true,
+            })]
+fn binary_search(arr: &VecWrapperI32, elem: &i32) -> UsizeOption {
+    let mut size = arr.len();
+    let mut base = 0;
+
+    let mut result = UsizeOption::None;
+    let mut continue_loop = size > 0;
+
+
+    while continue_loop {
+        body_invariant!(continue_loop == (size > 0 && result.is_none()));
+        body_invariant!(base + size <= arr.len());
+        body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
+            arr.lookup(k1) <= arr.lookup(k2)));
+        body_invariant!(forall(|k: usize| (0 <= k && k < base) ==> arr.lookup(k) < *elem));
+        body_invariant!(result.is_none() ==>
+                (forall(|k: usize| (base + size <= k && k < arr.len()) ==> *elem != arr.lookup(k))));
+        body_invariant!(match result {
+                    UsizeOption::Some(index) => (
+                        0 <= index && index < arr.len() &&
+                        arr.lookup(index) == *elem
+                    ),
+                    UsizeOption::None => true,
+                });
+        let half = size / 2;
+        let mid = base + half;
+
+        let mid_element = arr.index(mid);
+        let cmp_result = cmp(mid_element, elem);
+        base = match cmp_result {
+            Less    => {
+                mid
+            },
+            Greater => {
+                base
+            },
+            // Equal
+            _   => {
+                result = UsizeOption::Some(mid);
+                base   // Just return anything because we are finished.
+            }
+        };
+
+        size -= half;
+        continue_loop = size > 0 && result.is_none();
+    }
+
+    result
+}
+
+fn main() {}
diff --git a/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs
new file mode 100644
index 00000000000..b13b9852458
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/rosetta/Binary_search/artefact_Binary_search_shared_monomorphised_fixed_termination.rs
@@ -0,0 +1,144 @@
+// compile-flags: -Puse_more_complete_exhale=false
+
+//! A copy of `artefact_Binary_search_shared.rs` with fixed non-termination bug and manually
+//! encoded termination check.
+
+use prusti_contracts::*;
+
+pub struct VecWrapperI32{
+    v: Vec<i32>
+}
+
+impl VecWrapperI32 {
+    #[trusted]
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.v.len()
+    }
+
+    #[trusted]
+    #[pure]
+    #[requires(0 <= index && index < self.len())]
+    pub fn lookup(&self, index: usize) -> i32 {
+        self.v[index]
+    }
+
+    #[trusted]
+    #[requires(0 <= index && index < self.len())]
+    #[ensures(self.lookup(index) == *result)]
+    pub fn index(&self, index: usize) -> &i32 {
+        &self.v[index]
+    }
+}
+
+pub enum UsizeOption {
+    Some(usize),
+    None,
+}
+
+impl UsizeOption {
+    #[pure]
+    pub fn is_some(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => true,
+            UsizeOption::None => false,
+        }
+    }
+    #[pure]
+    pub fn is_none(&self) -> bool {
+        match self {
+            UsizeOption::Some(_) => false,
+            UsizeOption::None => true,
+        }
+    }
+}
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+use self::Ordering::*;
+
+#[ensures(match result {
+                Equal => *a == *b,
+                Less => *a < *b,
+                Greater => *a > *b,
+            })]
+fn cmp(a: &i32, b: &i32) -> Ordering {
+    if *a == *b { Equal }
+        else if *a < *b { Less }
+            else { Greater }
+}
+
+
+#[requires(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
+             arr.lookup(k1) <= arr.lookup(k2)))]
+#[ensures(result.is_none() ==>
+            (forall(|k: usize| (0 <= k && k < arr.len()) ==> *elem != arr.lookup(k))))]
+#[ensures(match result {
+                UsizeOption::Some(index) => (
+                    0 <= index && index < arr.len() &&
+                    arr.lookup(index) == *elem
+                ),
+                UsizeOption::None => true,
+            })]
+fn binary_search(arr: &VecWrapperI32, elem: &i32) -> UsizeOption {
+    let mut size = arr.len();
+    let mut base = 0;
+
+    let mut result = UsizeOption::None;
+    let mut continue_loop = size > 0;
+
+
+    while continue_loop {
+        body_invariant!(continue_loop == (size > 0 && result.is_none()));
+        body_invariant!(base + size <= arr.len());
+        body_invariant!(forall(|k1: usize, k2: usize| (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
+            arr.lookup(k1) <= arr.lookup(k2)));
+        body_invariant!(forall(|k: usize| (0 <= k && k < base) ==> arr.lookup(k) < *elem));
+        body_invariant!(result.is_none() ==>
+                (forall(|k: usize| (base + size <= k && k < arr.len()) ==> *elem != arr.lookup(k))));
+        body_invariant!(match result {
+                    UsizeOption::Some(index) => (
+                        0 <= index && index < arr.len() &&
+                        arr.lookup(index) == *elem
+                    ),
+                    UsizeOption::None => true,
+                });
+        let ghost_old_size = size;
+
+        let half = size / 2;
+        let mid = base + half;
+
+        let mid_element = arr.index(mid);
+        let cmp_result = cmp(mid_element, elem);
+        base = match cmp_result {
+            Less    => {
+                mid
+            },
+            Greater => {
+                base
+            },
+            // Equal
+            _   => {
+                result = UsizeOption::Some(mid);
+                base   // Just return anything because we are finished.
+            }
+        };
+
+        if half == 0 {
+            break;
+        }
+
+        size -= half;
+        continue_loop = size > 0 && result.is_none();
+
+        prusti_assert!(ghost_old_size >= 0 && ghost_old_size > size);   // Termination check.
+    }
+
+    result
+}
+
+fn main() {}