Fix for bug 444, dealing with the placing of set-logic in dumping modes.

CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report.

This also fixes a memory leak in the new-variable-notification mechanism.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 9 insertions, 1 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5c383071a..b2ac0b886 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -149,6 +149,14 @@ class CVC4_PUBLIC SmtEngine {
   smt::CommandList* d_modelCommands;
 
   /**
+   * A vector of declaration commands waiting to be dumped out.
+   * Once the SmtEngine is fully initialized, we'll dump them.
+   * This ensures the declarations come after the set-logic and
+   * any necessary set-option commands are dumped.
+   */
+  std::vector<Command*> d_dumpCommands;
+
+  /**
    * The logic we're in.
    */
   LogicInfo d_logic;
@@ -295,7 +303,7 @@ class CVC4_PUBLIC SmtEngine {
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
-  void addToModelCommand(Command* c);
+  void addToModelCommandAndDump(const Command& c, const char* dumpTag = "declarations");
 
   /**
    * Get the model (only if immediately preceded by a SAT