include assertion

kroening · kroening · commit 1caed7870b20 · 2015-02-04T20:14:00.000Z
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5163 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -125,7 +125,9 @@ void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
       if(solver.l_get(cond).is_false())
       {
         g.failed=true;
-        build_goto_trace(bmc.equation, *c_it, solver, bmc.ns, g.goto_trace);
+        symex_target_equationt::SSA_stepst::iterator next=*c_it;
+        next++; // include the assertion
+        build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace);
         break;
       }
     }

Original file line number	Diff line number	Diff line change
`@@ -125,7 +125,9 @@ void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)`
`125`	`125`	`if(solver.l_get(cond).is_false())`
`126`	`126`	`{`
`127`	`127`	`g.failed=true;`
`128`		`- build_goto_trace(bmc.equation, *c_it, solver, bmc.ns, g.goto_trace);`
	`128`	`+ symex_target_equationt::SSA_stepst::iterator next=*c_it;`
	`129`	`+ next++; // include the assertion`
	`130`	`+ build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace);`
`129`	`131`	`break;`
`130`	`132`	`}`
`131`	`133`	`}`