1 files changed, 14 insertions, 8 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 467b150d3..485a478d8 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -76,14 +76,20 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(q != NULL) {
     d_result = res = q->getResult();
   }
-  // dump the model if option is set
-  if( status &&
-      d_options[options::produceModels] &&
-      d_options[options::dumpModels] &&
-      ( res.asSatisfiabilityResult() == Result::SAT ||
-        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
-    Command* gm = new GetModelCommand();
-    status = doCommandSingleton(gm);
+  // dump the model/proof if option is set
+  if(status) {
+    if( d_options[options::produceModels] &&
+        d_options[options::dumpModels] &&
+        ( res.asSatisfiabilityResult() == Result::SAT ||
+          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+      Command* gm = new GetModelCommand();
+      status = doCommandSingleton(gm);
+    } else if( d_options[options::proof] &&
+               d_options[options::dumpProofs] &&
+               res.asSatisfiabilityResult() == Result::UNSAT ) {
+      Command* gp = new GetProofCommand();
+      status = doCommandSingleton(gp);
+    }
   }
   return status;
 }