1 files changed, 13 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index f1742b549..556e51216 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -19,6 +19,8 @@
 
 #include "main/main.h"
 
+#include "smt/options.h"
+
 namespace CVC4 {
 namespace main {
 
@@ -64,6 +66,17 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
+  //dump the model if option is set
+  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
+    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
+         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
+        Command * gm = new GetModelCommand;
+        status = doCommandSingleton(gm);
+      }
+    }
+  }
   return status;
 }