Massive slowdown and weird number of symbols when doing symbolic allocations

[krtab]

When running code-examples/rust/cross_language_hash from https://github.com/zapashcanon/paper-owi24/tree/issue_symbolic_memory we get the following weird output:

Trap: memory heap buffer overflow
Model:
  (model
    (symbol_0 (i32 1))
    (symbol_23 (i32 1205)))

[redianthus]

What do you mean by a massive slowdown? Is this by comparing two different Owi versions?

What would you expect regarding symbols ? The following:

Trap: memory heap buffer overflow
Model:
  (model
    (symbol_0 (i32 1))
    (symbol_1 (i32 1205)))

?

[filipeom]

What do you mean by a massive slowdown? Is this by comparing two different Owi versions?

Between:

    let user_name_size = owi_sym::u32_symbol() as usize;
    owi_sym::assume(user_name_size == 1); // Creating a symbol == 1
    // let user_name_size = 1;            // And using a concrete variable

What would you expect regarding symbols ? The following:

Trap: memory heap buffer overflow Model: (model (symbol_0 (i32 1)) (symbol_1 (i32 1205)))

?

Yes, something like this.

[redianthus]

@S41d this may be something that gets fixed by your PR about scopes, we should have a look at it together at some point