Minor but correction in sigali output.
- Translation to z3z now evaluates constant expressions instead of abstracting them. This non-feature could cause "false" synthesis failures due to non-translatable yet constant expressions possibly introduced by tomato (or manually), for instance `not false' in node `n' bellow: node n (a: bool) returns (ok: bool) contract assume true enforce ok with () let ok = a or not false; tel
This commit is contained in:
parent
899d33afb6
commit
8497bafa2e
|
@ -61,7 +61,7 @@ let current_inputs : IdentSet.t ref = ref IdentSet.empty
|
||||||
let current_locals : IdentSet.t ref = ref IdentSet.empty
|
let current_locals : IdentSet.t ref = ref IdentSet.empty
|
||||||
|
|
||||||
let translate_static_exp se =
|
let translate_static_exp se =
|
||||||
match se.se_desc with
|
match (Static.simplify QualEnv.empty se).se_desc with
|
||||||
| Sint(v) -> Cint(v)
|
| Sint(v) -> Cint(v)
|
||||||
| Sfloat(_) -> raise Untranslatable
|
| Sfloat(_) -> raise Untranslatable
|
||||||
| Sbool(true)
|
| Sbool(true)
|
||||||
|
|
Loading…
Reference in a new issue