SRI-CSL / yices2 / 25418071995

67%

master: 67%

Build Type

Pull #623

github

Committed by ahmed-irfan

Commit Message

smt2: address review feedback on algebraic printer (PR #623)

- Assert that libpoly isolating intervals are always strictly open
  (a_open == b_open == 1), matching root-of-with-interval's
  exclusive-bound convention; catches any future libpoly change
- Add comment above smt2_pp_algebraic citing the SMT-COMP 2026
  model-validation format spec
- Cast size_t q->n to unsigned long explicitly before passing to
  mpz_ui_pow_ui to silence truncation warnings on LLP64 targets

Pull Request Pull Request #623: smt2: print algebraic numbers in SMT-COMP 2026 root-of-with-interval …

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%)

1643495.28 hits per line