SRI-CSL / yices2 / 30150074613

71%

Build Type

push

github

Committed by web-flow

Commit Message

Fix ef-solve crash and spurious "model error" on UF-in-arithmetic quantifiers (#657) (#658)

ef-solve on a forall body with an uninterpreted-function application inside
arithmetic (e.g. (f x) in (< x C)) crashed, and on release builds aborted with
a bogus "FATAL ERROR: ... model error" bug report. Two independent causes:

- quant_pattern.c walked terms with term_child, which only supports composite
  terms. Arithmetic/bitvector polynomials, products, and projections (which
  term_num_children still counts) hit term_child's composite path and read a
  wrong descriptor -> ASan/debug crash, release UB. Add a shared
  term_ith_subterm() in term_explorer.c that reads those components off the
  descriptor, and use it in the three quant pattern walkers.

- ef_generalize3 built a full model via yices_model_from_map, which rejects
  function-typed existentials. For a problem with an uninterpreted-function
  existential and arithmetic universals (unsupported by projection-based
  generalization) this is now reported as 'unknown' instead of a fatal bug.

Adds regression test tests/regress/efsmt/ef-tests/iss657.ys.

Coverage Stats

29 of 46 new or added lines in 3 files covered. (63.04%)

1 existing line in 1 file now uncovered.

95573 of 134216 relevant lines covered (71.21%)

1669601.34 hits per line