diff options
| author | Alasdair Armstrong | 2019-04-17 15:54:52 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-17 16:22:45 +0100 |
| commit | b8f0a4e79749278f18e2e98f87a817e27a15c9ef (patch) | |
| tree | 57a50fb4fe639d414dcfbcf2949ee52cb88387bb /src/jib/c_backend.mli | |
| parent | bcf2221ba51a3df93c96e3f4a1e779079914d68d (diff) | |
SMT: Support generic vectors and handle lets between specs and functions
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.
Diffstat (limited to 'src/jib/c_backend.mli')
0 files changed, 0 insertions, 0 deletions