From 442cf66fdc084e16aa366ba228fb3fe6f6035598 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Tue, 3 May 2016 17:49:27 -0700
Subject: [PATCH] don't fail when nullifying a var not in the prop

Reviewed By: jeremydubreil

Differential Revision: D3243449

fb-gh-sync-id: c8f92d2
fbshipit-source-id: c8f92d2
---
 infer/src/backend/symExec.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 2f2b781f0..d5df7d5e6 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1220,7 +1220,11 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               | true -> sigma' in
             let eprop_res = Prop.replace_sigma sigma'' eprop in
             ret_old_path [Prop.normalize eprop_res]
-        | _ -> assert false
+        | [], _ ->
+            ret_old_path [prop_]
+        | _ ->
+            L.err "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp pe_text) pvar;
+            assert false
       end
   | Sil.Abstract _ ->
       let node = State.get_node () in