}
}
- if(options::incrementalSolving() && options::proof()) {
- Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl;
- setOption("incremental", SExpr("false"));
- }
-
if (options::proof())
{
+ if (options::incrementalSolving())
+ {
+ if (options::incrementalSolving.wasSetByUser())
+ {
+ throw OptionException("--incremental is not supported with proofs");
+ }
+ Warning()
+ << "SmtEngine: turning off incremental solving mode (not yet "
+ "supported with --proof, try --tear-down-incremental instead)"
+ << endl;
+ setOption("incremental", SExpr("false"));
+ }
if (d_logic > LogicInfo("QF_AUFBVLRA")) {
throw OptionException(
"Proofs are only supported for sub-logics of QF_AUFBVLIA.");
regress0/nl/very-easy-sat.smt2
regress0/nl/very-simple-unsat.smt2
regress0/options/invalid_dump.smt2
+ regress0/options/invalid_option_inc_proofs.smt2
regress0/opt-abd-no-use.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2