use these overflow predicates instead of compiler-generated conditions, e.g., y != 0 and x * y / y != x for x * y. this may improve smt solver performance, as it enables solvers to utilize better encoding or methodologies for reasoning about overflows.
in the next SMT-LIB version 2.7, overflow predicates will be added.
use these overflow predicates instead of compiler-generated conditions, e.g.,
y != 0 and x * y / y != xforx * y. this may improve smt solver performance, as it enables solvers to utilize better encoding or methodologies for reasoning about overflows.