[Eva] Evaluation engine: refactors function [assume_valid_div].

Also documents that the behavior of a%b depends on the behavior of a/b.