Regarding question 1, the option :incremental
is not part of the SMT-LIB 2.0 standard. The standard defines/suggests a small set of options that should be supported by all solvers, and :incremental
is not one of them. This is probably a CVC4 specific option. Z3 just ignores this command. Moreover, Z3 does not need the user to enable incremental solving.
Regarding question 2, the SMT-LIB 2.0 standard says there are 3 possible outputs for the check-sat
: unsat
, sat
and unknown
. The unknown
result is used when a solver did not manage to establish whether the set of assertions is satisfiable or not. Some solvers produce a "candidate model" even when they produce unknown
.
As far as I know, MathSAT 5 does not support quantifiers yet. However, this should change in the future.