SMT solving is not invoked with `--incremental-loop` about cbmc HOT 2 OPEN

IIRC the incremental mode works with MiniSAT because the SMT back-end is very much one-shot. The work that @thomasspriggs was doing on the new SMT back-end would resolve that in the longer term.

from cbmc.

Looks like this should work with the new incremental SMT back end with a few minor fixes -

• Some command line argument / option fixing to ensure the correct decision procedure is used. The "refine" option causes a SAT based bv_refinementt to be used in solver_factory.cpp even when an SMT solver is specified. I think "refine" and SMT options should probably be considered to be mutually exclusive and hence generate a usage error. The current behaviour is to ignore the SMT argument as outlined in this issue.
• The --incremental-loop argument in cbmc_parse_options.cpp automatically switches on the refine and refine-arrays options. This doesn't necessarily seem to be desirable behaviour; particularly given the aforementioned incompatibilities.
• The single_loop_incremental_symex_checkert currently uses the push() and pop() interface of the decision procedure. A minor change to implement this in the new SMT decision procedure is required. As incremental solving is supported along with push and pop in the AST the implementation is trivial -

void smt2_incremental_decision_proceduret::push()
{
  solver_process->send(smt_push_commandt{1});
}

void smt2_incremental_decision_proceduret::pop()
{
  solver_process->send(smt_pop_commandt{1});
}

from cbmc.