Commit bdad4394 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Avoid creating trivial VCs.

parent 4c9a7905
...@@ -491,7 +491,7 @@ and wp_desc env rm e q = match e.expr_desc with ...@@ -491,7 +491,7 @@ and wp_desc env rm e q = match e.expr_desc with
with Exit -> with Exit ->
let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) in let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) in
let w3 = wp_expr env rm e3 (filter_post e3.expr_effect q) in let w3 = wp_expr env rm e3 (filter_post e3.expr_effect q) in
t_if test w2 w3 t_if_simp test w2 w3
in in
let q1 = saturate_post e1.expr_effect (res, q1) q in let q1 = saturate_post e1.expr_effect (res, q1) q in
wp_expr env rm e1 q1 wp_expr env rm e1 q1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment