Project

General

Profile

Revision df39e35a src/normalization.ml

View differences:

src/normalization.ml
372 372
     - compute the associated expression without aliases     
373 373
  *)
374 374
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
375
  let split_defs = Splitting.tuple_split_eq_list defs in
376 375
  let norm_traceability = {
377 376
    annots = List.map (fun v ->
378 377
      let eq =
379 378
	try
380
	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs 
379
	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
381 380
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
      let expr = substitute_expr diff_vars split_defs eq.eq_rhs in
381
      let expr = substitute_expr diff_vars defs eq.eq_rhs in
383 382
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
384 383
      (["horn_backend";"trace"], pair)
385 384
    ) [] (*diff_vars*);

Also available in: Unified diff