Ignore:
Timestamp:
Mar 15, 2013, 7:22:17 PM (7 years ago)
Author:
tranquil
Message:

Corrected bug where eliminable statements where not eliminated. Changed eliminable output from option label to bool.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2883 r2887  
    350350  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
    351351  let move ≝ move globals localss carry_lives_after in
     352  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
    352353  match s with
    353354  [ step_seq s' ⇒
Note: See TracChangeset for help on using the changeset viewer.