SmtEngine now fails with a ModalException if --incremental is not enabled

but a push/pop or multiple query is attempted (previously it could give
incorrect answers)

Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).

Also fix mkbuilddir script for when it's called from contrib/switch-config.

1 files changed, 16 insertions, 3 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d8d9f4b54..b8a72dc38 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -125,12 +125,20 @@ class CVC4_PUBLIC SmtEngine {
   std::string d_logic;
 
   /**
-   * Whether or not we have added any
-   * assertions/declarations/definitions since the last checkSat/query
-   * (and therefore we're not responsible for an assignment).
+   * Whether or not we have added any assertions/declarations/definitions
+   * since the last checkSat/query (and therefore we're not responsible
+   * for an assignment).
    */
   bool d_haveAdditions;
 
+  /**
+   * Whether or not a query() or checkSat() has already been made through
+   * this SmtEngine.  If true, and d_incrementalSolving is false, then
+   * attempting an additional query() or checkSat() will fail with a
+   * ModalException.
+   */
+  bool d_queryMade;
+
   /** 
    * Whether or not to type check input expressions.
    */
@@ -157,6 +165,11 @@ class CVC4_PUBLIC SmtEngine {
   bool d_produceAssignments;
 
   /**
+   * Whether multiple queries can be made, and also push/pop is enabled.
+   */
+  bool d_incrementalSolving;
+
+  /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
   Result d_status;