invariant_sett invariant_set
goto_programt::const_targett locationt
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
virtual void transform(const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...