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

[ahmed-irfan]

Fixes #403.

get-value on a function/array term segfaults in QF_AUFBV (CDCL(T) solver).

Cause

When building a model, a function/array's default value (its value outside the explicitly-mapped domain) is a fresh particle of the range type. egraph_concretize_value realizes it with make_fresh_value, which returns null_value for a finite range whose values are all already used in the value table (in the report, range BitVec 2 — all 4 values taken). That null_value (-1) was passed unchecked to vtbl_mk_function as the default, crashing (in debug: assert(good_object(table, def)) at concrete_values.c:2445).

Fix

When no fresh value exists, fall back to vtbl_make_object. This is sound: 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). Mirrors the existing mcsat uf_plugin.c pattern (vtbl_make_object for finite types, make_fresh_value only for infinite ones).

Verification

• Debug and release builds no longer crash; return sat with a valid model.
• Model cross-checked with z3: pinning all base state values from yices's model keeps the constraints SAT (valid witness).
• Full regression suite passes (1765/0); arrays tests clean under the assert-enabled build.
• Added regression test tests/regress/iss403.smt2 (+ .gold).

[coveralls]

coverage: 71.213% (+0.002%) from 71.211% — elipparini:fix/issue-403-getvalue-segfault into SRI-CSL:master