From b62c3f55b9ca1f7f9b9cc062321bc49d4cb3d713 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 8 Sep 2020 09:37:55 -0700 Subject: [PATCH] [pulse] fix fuel debug message Summary: This would previously print that we ran out of fuel even if we didn't and we simply reached a normal form. Reviewed By: ezgicicek Differential Revision: D23575571 fbshipit-source-id: 37d02ca8d --- infer/src/pulse/PulseFormula.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index c72ebab7d..b3525cffa 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1200,13 +1200,15 @@ end = struct fuel). That's ok because there's not much fuel to begin with, and as long as we're making progress it's probably worth it anyway. *) let rec normalize_with_fuel ~fuel phi = - let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in - if new_linear_eqs && fuel > 0 then ( - L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ; - normalize_with_fuel ~fuel:(fuel - 1) phi ) - else ( + if fuel <= 0 then ( L.d_printfln "ran out of fuel when normalizing" ; Sat phi ) + else + let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in + if new_linear_eqs then ( + L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ; + normalize_with_fuel ~fuel:(fuel - 1) phi ) + else Sat phi in normalize_with_fuel ~fuel:base_fuel phi