This directory contains examples to test the inference
of arithmetic non-fail conditions, i.e., where an SMT solver
(here: Z3) is used to verify the satisfaction of these conditions.