Don't apply field sensitivity on index expression writing

romainbrenguier · romainbrenguier · commit 09bff09c56bd · 2019-06-03T09:08:42.000+01:00
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
@@ -127,7 +127,7 @@ exprt field_sensitivityt::apply(
           else
             return std::move(tmp);
         }
-        else
+        else if(!write)
         {
           // Expand the array and return `{array[0]; array[1]; ...}[index]`
           exprt expanded_array =

Original file line number	Diff line number	Diff line change
`@@ -127,7 +127,7 @@ exprt field_sensitivityt::apply(`
`127`	`127`	`else`
`128`	`128`	`return std::move(tmp);`
`129`	`129`	`}`
`130`		`- else`
	`130`	`+ else if(!write)`
`131`	`131`	`{`
`132`	`132`	// Expand the array and return `{array[0]; array[1]; ...}[index]`
`133`	`133`	`exprt expanded_array =`