From d375a6c03eab80f396d49617c9cd32f26575afaa Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 28 Jan 2021 06:47:57 -0800 Subject: [PATCH] [pulse] also compare path conditions when comparing states Summary: States would be considered equal when they describe the same heap shape even though their path conditions were different. Not good. Reviewed By: skcho Differential Revision: D26022135 fbshipit-source-id: 510913cde --- infer/src/pulse/PulseAbductiveDomain.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 773260d84..4db8ba346 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -122,6 +122,7 @@ let leq ~lhs ~rhs = phys_equal lhs rhs || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls && ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status) + && PathCondition.equal lhs.path_condition rhs.path_condition && match BaseDomain.isograph_map BaseDomain.empty_mapping