Open
Description
The closure check for deductions does not work correctly with the following domain operation.
domain(true_exprt(), all_vars, old_val, new_val, deductions)
Here statement = true_exprt
and all_vars
contains all variables in the program, which is the sub-domain. So, we want to find all transitive dependencies when domain=subdomain
. The problem may be due to following two cases:
1> Incorrect creation of sub-domain
2> when true_exprt()
is popped, there is no variable in the statement to project on.