In the Gauss example, sum(n) terminates /n. As all TRIL scalars are machine word bitvectors, TRIL sum can only be something like bv32→bv32. Currently, a termination metric can't be anything other than int, so we are forced to call Z3_mk_bv2int which means switching from the fast bit-fiddling SAT solver to the general uninterpreted/incremental SMT core.
In the Gauss example,
sum(n)terminates/n. As all TRIL scalars are machine word bitvectors, TRILsumcan only be something likebv32→bv32. Currently, a termination metric can't be anything other thanint, so we are forced to callZ3_mk_bv2intwhich means switching from the fast bit-fiddling SAT solver to the general uninterpreted/incremental SMT core.