Skip to content

Commit be2709c

Browse files
consider assume statements during symbolic execution
Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
1 parent d59dd58 commit be2709c

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/goto-instrument/full_slicer.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,7 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
330330
{
331331
// some variables are used during symbolic execution only
332332

333+
if (target->is_assume()) return true;
333334
if(!target->is_assign()) return false;
334335

335336
const code_assignt &a=to_code_assign(target->code);

0 commit comments

Comments
 (0)