diff options
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r-- | src/main/command_executor.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 34b484910..4dc49ee53 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -100,6 +100,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) { Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); + } else if( d_options[options::dumpInstantiations] && + d_result.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gi = new GetInstantiationsCommand(); + status = doCommandSingleton(gi); } } return status; |