Commit d5670dc8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Mark functions containing if-then-else as nonlinear.

Indeed their inlining causes an exponential growth of the formulas for all
the provers that are relying on the "eliminate_if" transformation.
parent 7ff10f73
......@@ -154,6 +154,7 @@ let eval_match ~inline kn t =
let rec linear vars t = match t.t_node with
| Tvar x -> Svs.add_new Exit x vars
| Tif _ -> raise Exit
| _ -> t_fold linear vars t
let linear t =
......
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