SMT solver returned unexpected status 1 with var

[Timmmm]

The following code fails to compile:

default Order dec

$include <prelude.sail>

bitfield BF : bits(8) = {
  T : 7 .. 0,
}

type full_width : Int = 10
let  full_width = sizeof(full_width)

function foo() -> bits(full_width) = {
  let meta = Mk_BF(0x00);
  let FW = full_width;
  var T : bits(FW) = 0b00 @ meta[T];
  T
}

I get:

Error:
SMT solver returned unexpected status 1

If I change the var to a let it gives a more reasonable error:

Type error:
test.sail:15.10-18:
15 |  let T : bits(FW) = 0b00 @ meta[T];
   |          ^------^
   | Well-formedness check failed for type
   | 
   | Caused by test.sail:15.15-17:
   | 15 |  let T : bits(FW) = 0b00 @ meta[T];
   |    |               ^^
   |    | Undefined type synonym FW

Which makes me suspect I am not supposed to do that but there's some check on var missing.

If I change both FWs to 'FW then it works as expected, which makes sense. So I think this is just missing type checking.

[Alasdair]

Should be fixed now