Mcsat bugfixes

[Ovascos]

• missing static identifier for plugin functions in bool_plugin.c
• fixed function pointer type mismatch for mcsat_evaluator_t
• minor bugfixes

[coveralls]

coverage: 71.214% (+0.006%) from 71.208% — Ovascos:mcsat-bugfixes into SRI-CSL:master

[ahmed-irfan]

Approved. I built the branch and ran the tests.

• Debug build from scratch: clean, no warnings.
• make check: 1779 pass, 0 fail. mcsat-regress: 727 pass, 0 fail.

The evaluator fix is correct. Master stored a 5-parameter, non-const function pointer, then cast the struct to mcsat_evaluator_interface_t*. That call was undefined behavior. The first-member form removes it.

I also checked the changes the description does not list:

• Every explain_evaluation implementer and both call sites use the new signature.
• The new static symbols have no reference outside their own file.
• 0.999F and 1e20F give the same bit patterns as before. Both fields are already float.
• The bool_plugin.c reformat is whitespace only. git diff -w shows no change.
• The removed trail_size parameter was never read. The removed model_queries.h include was a duplicate.

One non-blocking comment is inline.

[ahmed-irfan]

This is the right fix. The same defect is still in this file.

solver_new_variable_notify_t (line 71) declares new_variable with a struct solver_new_variable_notify_s* first parameter. Line 966 casts the struct to variable_db_new_variable_notify_t*. variable_db.c:62 then calls the pointer through the interface type. The two function types are incompatible, so that call is undefined behavior. It is the same class you fix here.

The same fix works: make variable_db_new_variable_notify_t notify_interface; the first member.

I checked the other interface casts in src/mcsat/. The (plugin_context_t*) and (trail_token_t*) casts use the safe first-member form. This one is the only outlier left. Non-blocking.