SRI-CSL / yices2 / 25359278986

67%

master: 69%

Build Type

push

github

Committed by ahmed-irfan

Commit Message

smt2: print algebraic numbers in SMT-COMP 2026 root-of-with-interval format

Previously, algebraic model values were printed as lossy float
approximations (e.g. 1.414214). The SMT-COMP 2026 model validation
track requires the root-of-with-interval format, which encodes the
exact value as a polynomial plus an isolating interval.

The new smt2_pp_algebraic normalizes the polynomial at print time
(square-free part via gcd(f,f'), then primitive part for coprime
coefficients with positive leading coefficient) and formats it as

  (root-of-with-interval (coeffs p_0 ... p_n) min max)

where coefficients are listed in ascending degree order and bounds are
SMT2 real literals (a.0 or (/ a.0 2^k.0) for dyadic rationals).
Rational algebraic values (f == NULL in libpoly) are printed directly
as real literals. Normalization happens only when a model is printed,
so solving performance is unaffected.

Two regression tests are added: one for a proper algebraic value (√2)
and one for the rational branch (x²=4, x>0 → 2.0). Four existing gold
files are updated to the new format.

Coverage Stats

74 of 78 new or added lines in 1 file covered. (94.87%)

27 existing lines in 2 files now uncovered.

83511 of 125222 relevant lines covered (66.69%)

1644169.41 hits per line