Abstraction options not working

[zhassan-aws]

I tried this code:

fn main() {
    let mut v = Vec::<u8>::new();
    v.push(5);
    assert!(v.len() == 1);
    let x = v.pop().unwrap();
    assert!(x == 5);
}

using the following command line invocation:

rmc test.rs --use-abs --abs-type no-back

with RMC version: 8de5cd67609

I expected to see this happen: The assert!(x == 5) should fails since the no-back abstraction doesn't store elements in the vector and returns a non-det value on pop (library/rmc/stubs/Rust/vec/noback_vec.rs):

   pub fn pop(&mut self) -> Option<T> {
        if self.len == 0 {
            None
        } else {
            self.len -= 1;
            Some(rmc::nondet::<T>())
        }
    }

Instead, this happened: The assertion passed and verification was successful.

If I explicitly include the noback_vec.rs file:

include!("/home/ubuntu/git/rmc/library/rmc/stubs/Rust/vec/noback_vec.rs");

The assertion fails.

[celinval]

Once we fix this, we should ensure that we add the stub tests are included in the regression.