1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3edcd6872..fecfba14a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -47,7 +47,7 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
-class NodeHashFunction;
+struct NodeHashFunction;
 
 class Command;
 class GetModelCommand;
@@ -77,7 +77,7 @@ namespace smt {
    */
   class DefinedFunction;
 
-  class SmtEngineStatistics;
+  struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
   class BooleanTermConverter;
@@ -444,7 +444,7 @@ public:
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
    */
-  Expr getValue(const Expr& e) throw(ModalException, LogicException);
+  Expr getValue(const Expr& e) throw(ModalException, TypeCheckingException, LogicException);
 
   /**
    * Add a function to the set of expressions whose value is to be