The Tuesday Afternoon Catch-All Commit (TACAC):

* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)

* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).

* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)

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

1 files changed, 8 insertions, 1 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index e20edfb42..460e3f1dc 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -345,10 +345,17 @@ public:
   /**
    * Make a tuple type with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> must
-   * have at least 2 elements.
+   * have at least one element.
    */
   TupleType mkTupleType(const std::vector<Type>& types);
 
+  /**
+   * Make a symbolic expressiontype with types from
+   * <code>types[0..types.size()-1]</code>.  <code>types</code> may
+   * have any number of elements.
+   */
+  SExprType mkSExprType(const std::vector<Type>& types);
+
   /** Make a type representing a bit-vector of the given size. */
   BitVectorType mkBitVectorType(unsigned size) const;