From d14ff99f45eb1fb76e909294cd9e2b981eb7b7d2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 1 May 2020 03:58:02 -0700 Subject: [PATCH] [pudge] try harder to prove false Summary: This gives more precision in tests. Reviewed By: jberdine Differential Revision: D21332072 fbshipit-source-id: df20daff3 --- infer/src/pulse/PulseSledge.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseSledge.ml b/infer/src/pulse/PulseSledge.ml index cce4fc5d2..b85fc3767 100644 --- a/infer/src/pulse/PulseSledge.ml +++ b/infer/src/pulse/PulseSledge.ml @@ -136,7 +136,11 @@ let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero (* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *) let is_unsat {eqs; non_eqs} = - Equality.is_false (Lazy.force eqs) || Term.is_false (Lazy.force non_eqs) + (* [Term.is_false] is cheap, forcing [eqs] is expensive, then calling [Equality.normalize] is + expensive on top of that *) + Term.is_false (Lazy.force non_eqs) + || Equality.is_false (Lazy.force eqs) + || Term.is_false (Equality.normalize (Lazy.force eqs) (Lazy.force non_eqs)) let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =