Whenever the constrained method behavior is invoked, the constrains should be added into the constraint space to explore them actively.
Or setup a passive approach (which could result is less state space to explore, but is much more complex. If the result could be treated as an independent symbolic value (only if at least one of the arguments is actually a symbolic value) with constraint condition => result. Of course the value should have to be constrained to a set of possible values (specified by the behavior). A problem could arise because of the solution with constrained method result variables - each constraint on a specific method is a different variable.
Whenever the constrained method behavior is invoked, the constrains should be added into the constraint space to explore them actively.
Or setup a passive approach (which could result is less state space to explore, but is much more complex. If the result could be treated as an independent symbolic value (only if at least one of the arguments is actually a symbolic value) with constraint
condition => result. Of course the value should have to be constrained to a set of possible values (specified by the behavior). A problem could arise because of the solution with constrained method result variables - each constraint on a specific method is a different variable.