diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
| commit | cc01e2119801bbd4fd99548b79c297fa57a1977d (patch) | |
| tree | cf9c64efbc286089a898d93abb3150e79138e5a7 /src/main/command_executor_portfolio.cpp | |
| parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) | |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 7392b2b62..61447afe2 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -204,12 +204,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) } Debug("portfolio::outputmode") << "Mode is " << mode - << "lastWinner is " << d_lastWinner + << "lastWinner is " << d_lastWinner << "d_seq is " << d_seq << std::endl; if(mode == 0) { d_seq->addCommand(cmd->clone()); - Command* cmdExported = + Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], @@ -352,12 +352,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_result.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; } else if(mode == 2) { - Command* cmdExported = + Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); bool ret = smtEngineInvoke(d_smts[d_lastWinner], |