SMT-LIBv2 compliance updates:

* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
  (there were some minor differences from the spec)

1 files changed, 8 insertions, 1 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 4df9054a7..efb2425a1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -309,7 +309,7 @@ public:
    * Query information about the SMT environment.
    */
   SExpr getInfo(const std::string& key) const
-    throw(BadOptionException);
+    throw(BadOptionException, ModalException);
 
   /**
    * Set an aspect of the current SMT execution environment.
@@ -536,6 +536,13 @@ public:
   unsigned long getTimeRemaining() const throw(ModalException);
 
   /**
+   * Permit access to the underlying ExprManager.
+   */
+  ExprManager* getExprManager() const {
+    return d_exprManager;
+  }
+
+  /**
    * Permit access to the underlying StatisticsRegistry.
    */
   StatisticsRegistry* getStatisticsRegistry() const;