symbolic_bounded_model_checker_sierra passed in an example expected to fail

[acmLL]

Machine: Apple M1 Pro
OS: macOS Ventura 13.4
Cairo: cairo-compile 2.0.0-rc2

Hi,

I have installed thoth current version with interest in testing the symbolic model checker. By following the tutorial, in the 2nd example:

fn thoth_test_product(mut a: felt252) {
let c = a * 2;
assert(c == 11, '');
}

I have saved the file as test2.cairo, compiled and ran:

thoth-checker -f ./test2.sierra
[+] Thoth Symbolic bounded model checker

[PASS] test2::test2::thoth_test_product (test 1/1, time: 0.07s, paths: 4)

But it would be expected to get [FAIL]...

I am attaching the compiled file so you can see what can be happened.

Thanks!
test2.sierra.zip