[pulse] bump base_fuel to 10 to avoid under-normalising formulas

Summary:
10 seems better at no visible CPU cost. Not very scientific as this is
only one data point, but neither was choosing 5 in the first place.

Measurements on OpenSSL using Pulse.ISL:
```
$ time infer --pulse-only  --scheduler callgraph -j 2  --pulse-report-latent-issues --pulse-isl

| fuel | user time (s) | under-normalisation | latent issues |
|------+---------------+---------------------+---------------|
|    5 |           163 |                3074 |           160 |
|   10 |           158 |                  85 |           160 |
|   15 |           174 |                  32 |           160 |
|   20 |           186 |                  20 |           160 |
```

Reviewed By: skcho

Differential Revision: D27156497

fbshipit-source-id: 1114b8677
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 4436265f6b
commit f56f18350d

@ -1204,7 +1204,7 @@ module Formula = struct
(** an arbitrary value *) (** an arbitrary value *)
let base_fuel = 5 let base_fuel = 10
let solve_lin_eq new_eqs t1 t2 phi = let solve_lin_eq new_eqs t1 t2 phi =
solve_normalized_lin_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi solve_normalized_lin_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi

Loading…
Cancel
Save