Only export them for the logic evalution by the cvalue domain.

David Bühler authored 5 years ago and Michele Alberti committed 5 years ago

When the subdivision on a sub-expression [s] is performed according to [s] and
not according to the complete expression [e], we then reevaluate [e] with the
result of the subdivision. However, the valuation should be cleared before.
Otherwise, the reevaluation uses the cache and not the reduced values computed
by the subdivision.

David Bühler authored 5 years ago and Michele Alberti committed 5 years ago

Do not stop the subdivision if it can reduce the value of a sub-expression
*and* later subdivisions may improve the value of the complete expression
with this reduction.
If no other subdivision is planned, then stop the subdivision if it cannot
improve the value of the complete expression (as before).

In the function [initialize_variable_using_type].
Adds a constructor [Return] to [variable_kind] for the special variable that
stores the return value of a function call.

Share scripts among models.
More robust against script errors.

Allows for more efficient filtering.
Also enhanced frame conditions with typing for globals.