diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-29 11:32:29 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-29 11:32:29 -0500 |
commit | d542d80f1241341752ed1843b63799435642c6f2 (patch) | |
tree | 1ec8f68fa99405de49b11ad1140baf0bebd28890 /src/smt/smt_engine.cpp | |
parent | ff6d52af155e37e27bcc8a963ecf1c272067e1f2 (diff) |
Fix proofs build.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2e1d5de3c..07b30a87e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1140,6 +1140,11 @@ void SmtEngine::setLogicInternal() throw() { } } + if (options::incrementalSolving() && options::proof()) { + Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof" << endl; + setOption("incremental", SExpr("false")); + } + // datatypes theory should assign values to all datatypes terms if logic is quantified if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) { if( !options::dtForceAssignment.wasSetByUser() ){ |