diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-03 15:20:56 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-03 15:20:56 -0400 |
| commit | 2f4ffdb91aa9d6bc379c26eafed055334f505899 (patch) | |
| tree | 3f65961ef08c45c3f5e29bd8aad91798ec1f978a /src/main | |
| parent | 8dc1280a5161633fddfb8334811a86c911bb25c1 (diff) | |
| parent | ec2a8ad5e5be550f4f0c5c3be92ee20bf2977efa (diff) | |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/command_executor.cpp | 5 | ||||
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 5 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index fee7e23a2..4bbfe2762 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,6 +22,7 @@ #include "main/options.h" #include "smt/options.h" +#include "printer/options.h" #ifndef __WIN32__ # include <sys/resource.h> @@ -132,7 +133,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetProofCommand(); } else if( d_options[options::dumpInstantiations] && - res.asSatisfiabilityResult() == Result::UNSAT ) { + ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) { g = new GetInstantiationsCommand(); } else if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 8af0c452a..fde9c1c85 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -29,6 +29,7 @@ #include "main/portfolio.h" #include "options/options.h" #include "smt/options.h" +#include "printer/options.h" #include "cvc4autoconfig.h" @@ -371,7 +372,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); } else if( d_options[options::dumpInstantiations] && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { + ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) { Command* gi = new GetInstantiationsCommand(); status = doCommandSingleton(gi); } else if( d_options[options::dumpUnsatCores] && |