-
Johannes Kanig authored
On N121-024 we fixed a bug where a state was incorrectly reused during merge. The fix was to never reuse state when merging. This resulted in a performance drop. The new fix now marks states which should not be reused - basically states that come from raise - and when such a state is present during merging, we don't reuse. Otherwise, we reuse. This seems to get us the performance and passes all tests. Marking is implemented simply by a flag in states * mlw_wp.ml: (mark) allows to set the marked flag of a state (empty) empty state is not marked (havoc) havoc doesn't change marked state (merge_vars, merge_regs) new argument "marked", only create a new variable when marked is true, otherwise reuse (fast_wp) in the case of Eraise, mark the used state M415-042 pass labels down to conjunctions Why3 parser groups the loop invariants into a single formula. This patch allows to have the VC labels on every conjunct mlw_wp.ml (fastwp) call wp_expl instead of t_label
2afdad2c