sail/test/smt/let_intervene.unsat.sail, branch sail2 Formal specification language for ISAs SMT: Support generic vectors and handle lets between specs and functions 2019-04-17T15:22:45+00:00 Alasdair Armstrong 2019-04-17T14:54:52+00:00 b8f0a4e79749278f18e2e98f87a817e27a15c9ef If we have e.g. $property val prop : ... let X = 0 function prop(...) = X == ... then we need to ensure that let X is included when we generate the property. 
If we have e.g.

$property
val prop : ...

let X = 0

function prop(...) = X == ...

then we need to ensure that let X is included when we generate the
property.