summaryrefslogtreecommitdiff
path: root/src/main/command_executor.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r--src/main/command_executor.cpp12
1 files changed, 7 insertions, 5 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 241ca2b8f..5dbc50592 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -159,11 +159,13 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
getterCommands.emplace_back(new GetProofCommand());
}
- if (d_options.getDumpInstantiations() &&
- ((d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
- (res.asSatisfiabilityResult() == Result::SAT ||
- (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) ||
- res.asSatisfiabilityResult() == Result::UNSAT)) {
+ if (d_options.getDumpInstantiations()
+ && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
+ && (res.asSatisfiabilityResult() == Result::SAT
+ || (res.isUnknown()
+ && res.whyUnknown() == Result::INCOMPLETE)))
+ || res.asSatisfiabilityResult() == Result::UNSAT))
+ {
getterCommands.emplace_back(new GetInstantiationsCommand());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback