SRI-CSL / yices2 / 28931436466

71%

push

github

Fix segfault in get-value for function default over exhausted finite range (#403) (#655)

When building a model, a function/array's default value is a fresh
particle of the range type. egraph_concretize_value realized it with
make_fresh_value, which returns null_value for a finite range whose
values are all already used. The null_value (-1) was passed unchecked
to vtbl_mk_function, crashing on get-value in QF_AUFBV.

Fall back to vtbl_make_object when no fresh value exists: a function's
default outside its explicit domain can be any value of the range type,
and distinctness of function variables is enforced separately by
force_maps_to_differ (fun_solver.c).

4 of 4 new or added lines in 1 file covered. (100.0%)

95569 of 134201 relevant lines covered (71.21%)

1662885.86 hits per line