Unrecognized cval generating SMT using version 0.15

[rmn30]

I'm receiving an error when trying to generate SMT:

Error:
Unrecognised cval (zz42786/2, zz42784/2)

This worked in previous versions. I don't have a minimized test case yet.

[rmn30]

Looks like smt_cval is missing a case for V_tuple?

[rmn30]

Test case:

$property
function prop () -> bool = {
    let (x, y) = (true, false);
    x
}

sail -smt test.sail

Error:
Unrecognised cval (true, false)

[Alasdair]

It'll be this commit I think:

6c2c285

Solution should be to split the C.struct_value flag into that and a separate C.tuple_value flag, which would be the old behavior before that commit.

Another fix could be to apply our tuple->named struct rewrite before, so tuples are represented as SMTLIB datatypes.

[rmn30]

Thanks. I've implemented this locally and it appears to work but now I don't think there are any uses of C.tuple_value=true?

[rmn30]

https://github.com/rems-project/sail/tree/tuple_value

[Alasdair]

isla will use C.tuple_value=true, but it lives in a separate repository