Revision ed736b69
Added by Pierre-Loïc Garoche over 8 years ago
| src/normalization.ml | ||
|---|---|---|
| 379 | 379 |
annots = List.map (fun v -> |
| 380 | 380 |
let eq = |
| 381 | 381 |
try |
| 382 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs
|
|
| 382 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs)
|
|
| 383 | 383 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
| 384 |
let expr = substitute_expr diff_vars defs eq.eq_rhs in
|
|
| 384 |
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
|
|
| 385 | 385 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
| 386 | 386 |
(["traceability"], pair) |
| 387 | 387 |
) diff_vars; |
Also available in: Unified diff
Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init