RMC needs a __VERIFIER_assume predicate

[danielsn]

Requested feature: __VERIFIER_assume
Use case: Assuming things in harnesses
Link to relevant documentation (Rust reference, Nomicon, RFC): http://www.cprover.org/cprover-manual/modeling/assumptions/
Is this a breaking change? No

Test case:

fn __VERIFIER_assume(cond: bool) {
    unimplemented!()
}

fn __nondet<T>() -> T {
    unimplemented!()
}


fn main() {
    let i : i32 = __nondet();
    __VERIFIER_assume(i < 10);
    assert!(i < 20);
}