Model generation for arith, boolean, and uf theories via

(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.

2 files changed, 2 insertions, 2 deletions

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 004f0c9a9..70f1047f5 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -71,7 +71,7 @@ void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
                           VarNameAttr(), s)) {
         out << s;
       } else {
-        out << "var_" << d_id << "[" << this << "]";
+        out << "var_" << d_id;
       }
       if(types) {
         // print the whole type, but not *its* type
diff --git a/src/expr/type.h b/src/expr/type.h
index 435d640d0..453eaf5c4 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -216,7 +216,7 @@ public:
 
   /**
    * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
-   * Aall predicate types are also function types.
+   * All predicate types are also function types.
    * @return true if the type is a predicate type
    */
   bool isPredicate() const;