© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Symbolic execution is an effective technique for exploring paths ina program and reasoning about all possible values on those paths.However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to morethan one memory object. In such cases, symbolic execution typicallyforks execution into multiple states, one for each object to whichthe pointer could refer.In this paper, we propose a technique that avoids this expensiveforking by using asegmented memory model. In this model, mem-ory is split into segments, so that each symbolic pointer refers toobjects in a single segment. The size of the segments are bound by athreshold, in order to avoid expensive constraints. This results in amemory model where forking due to symbolic pointer dereferencesis significantly reduced, often completely.We evaluate our segmented memory model on a mix of wholeprogram benchmarks (such asm4andmake) and library bench-marks (such asSQLite), and observe significant decreases in execu-tion time and memory usage