A simple program involving BTreeSet runs out of memory

[zhassan-aws]

I tried this code:

use std::collections::BTreeSet;

fn main() {
    let mut set = BTreeSet::<u32>::new();
    set.insert(0);
}

using the following command line invocation:

rmc test.rs --unwind 2

with RMC version: 8de5cd67609

CBMC memory usage went up to 20GB after 1 minute and reached ~30 GB shortly after.

[zhassan-aws]

This got fixed by f088f9c, in particular the switch to use assert-false-assume-false for undefined functions as opposed to just assert-false.

[zhassan-aws]

Reopening: with e4851c1, memory usage exceeds 20 GB with an unwind of 3. With an unwind of 2, it finishes in a few minutes, but an unwinding assertion fails.

[tautschnig]

The changes in #1676 make an unwinding 2 terminate in 2.4 seconds (with the expected unwinding failure). An unwinding of 3 takes 3.1 seconds, no more unwinding failures.