I've updated this PR and added a change to --split_queries to make it tri-valued: no, on_failure (the default, equal to current behavior) and always (equivalent to passing --split_queries without any argument now).

The rationale is that sometimes it's desirable to prevent the split+retry process from happening, and just be notified of failures earlier.

Some refactoring of the discharging code is also present to ensure:

• The smt_sync() calls are not affected by --quake nor --split_queries, it is really close to just asking the solver and returning the answer. The only retrying that happens is increasing fuel, as for normal queries.
• When --split_queries always is on, the --quake test is independent for each of them.
• When --quake is on and --split_queries is on_failure (or wasn't given, as this is the default), then the splitting is actually OFF. The rationale is that quake is on when we're checking for robustness, not trying to solve one particular error, and the behavior would be unclear (are the split queries quake tested? does a success after splitting count as good for the quake test?). Plus, if one wants to quake test the individual sub queries, one can use --quake 100/k --split_queries always.

As discussed today I modified smt_sync to be more configurable. The primitive is now called t_smt_sync and takes an explicit vconfig, a structure which specifies fuels, rlimits, encoding options, etc. The old smt_sync is just t_smt_sync (get_vconfig()) and a smt_sync' takes an explicit fuel and ifuel and only does a single try to solve the query.

Differently from what was discussed today: I could have gone further and only have a single-shot smt_sync with all the fuel logic being done in tactics. I decided against this since it requires to duplicate the fuel-increasing logic in tactics (not too bad...), and also since the encoding would be slightly different. A fuel retry stays within the same (parent) push-pop context, while a separate smt_sync call would need to be in a different one. As the solver may be quite sensitive to these things (at least currently) I think we should stay closer to the normal discharging path.