Fix Z3 refcount leak in simple backend _sym_push_path_constraint

[Emad-Mahmodi]

Fixes the reference-count bug reported in eurecom-s3/symcc#180.

In the simple backend's _sym_push_path_constraint, the simplified constraint (inc_ref'd) and its negation not_constraint (inc_ref'd) are created, then one of them is selected as newConstraint and inc_ref'd a second time before being asserted:

Z3_ast newConstraint = (taken ? constraint : not_constraint);
Z3_inc_ref(g_context, newConstraint);
Z3_solver_assert(g_context, g_solver, newConstraint);
...
Z3_dec_ref(g_context, constraint);
Z3_dec_ref(g_context, not_constraint);
// newConstraint is never dec_ref'd

The two Z3_dec_ref calls balance constraint and not_constraint, but the extra inc_ref on newConstraint has no matching dec_ref, so one AST reference leaks per call. Refcount trace (taken == true, so newConstraint == constraint):

inc_ref(constraint)      -> 1
inc_ref(newConstraint)   -> 2
dec_ref(constraint)      -> 1
dec_ref(not_constraint)  -> 0  (freed, correct)
return: constraint stuck at 1, no owner  -> leaked reference

The fix adds the matching Z3_dec_ref(g_context, newConstraint);. The solver retains its own internal reference to the asserted constraint, so dropping the user reference to 0 keeps it asserted — the change is behavior-preserving. Verified: on a workload of 256 path constraints the set of diverging inputs found is byte-for-byte identical before and after the patch.

Honest note on impact: in the simple backend g_solver is never reset and the path constraint is asserted permanently, so the leaked reference is redundant with the solver's own retention and I did not observe a peak-RSS difference at this scale. This is therefore a correctness fix (the inc_ref/dec_ref discipline is simply wrong as written) rather than a measured performance fix; it matters in any context where the solver is reset/popped or where this pattern is reused.