SMT backend: struct getter generates "zUNKNOWN"

[PRugg-Cap]

The following code:

struct MyStruct = { f : bool }

let my_struct : MyStruct = struct { f = true }

$property
function prop() -> bool = my_struct.f

Generates the following SMT2 file (sail 0.18.0, sail -smt test.sail):

(declare-datatypes ((Unit 0)) (((unit))))
(declare-datatypes ((Bits 0)) (((Bits (len (_ BitVec 8)) (contents (_ BitVec 64))))))
(declare-datatypes ((Zexception 0)) (((z__dummy_exnz3 (unz__dummy_exnz3 Unit)))))
(declare-datatypes ((ZMyStruct 0)) (((ZMyStruct (ZMyStruct_zf Bool)))))
(assert (not (ZMyStruct_zf zUNKNOWN)))
(check-sat)

This then causes a z3 error: (error "line 5 column 27: unknown constant zUNKNOWN")

Apologies for raising multiple issues: I'm finally trying to use the refactored backend. Really appreciate your time on this!

[PRugg-Cap]

It hits https://github.com/rems-project/sail/blob/9fd675d56144e05e107aabb9c11ef0a8874c07f2/src/lib/smt_gen.ml#L381 if I uncomment the failwith. Looks like a V_struct case is missing?

[Alasdair]

Changing this line to false might work around it. Probably hadn't considered this case as I've mostly been using the SMT as an intermediate representation for SystemVerilog expressions, where there aren't any struct literals.

https://github.com/rems-project/sail/blob/9fd675d56144e05e107aabb9c11ef0a8874c07f2/src/sail_smt_backend/jib_smt.ml#L1246

[Alasdair]

Apologies for raising multiple issues: I'm finally trying to use the refactored backend. Really appreciate your time on this!

I appreciate it, there are probably lots of small issue right now that I just haven't hit, as I haven't really been using the generated SMT in anger.

[PRugg-Cap]

Changing this line to false might work around it.

Lifesaver! Thank you :)

[Alasdair]

Should be fixed by https://github.com/rems-project/sail/pull/675