1 files changed, 24 insertions, 2 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eba73c380..4ac21d392 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -587,11 +587,33 @@ class CVC4_PUBLIC SmtEngine
   /** Same as above, but without user-provided grammar restrictions */
   bool getAbduct(const Expr& conj, Expr& abd);
 
-  /** Get list of quantified formulas that were instantiated. */
+  /**
+   * Get list of quantified formulas that were instantiated on the last call
+   * to check-sat.
+   */
   void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs);
 
-  /** Get instantiations. */
+  /**
+   * Get instantiations for quantified formula q.
+   *
+   * If q was a quantified formula that was instantiated on the last call to
+   * check-sat (i.e. q is returned as part of the vector in the method
+   * getInstantiatedQuantifiedFormulas above), then the list of instantiations
+   * of that formula that were generated are added to insts.
+   *
+   * In particular, if q is of the form forall x. P(x), then insts is a list
+   * of formulas of the form P(t1), ..., P(tn).
+   */
   void getInstantiations(Expr q, std::vector<Expr>& insts);
+  /**
+   * Get instantiation term vectors for quantified formula q.
+   *
+   * This method is similar to above, but in the example above, we return the
+   * (vectors of) terms t1, ..., tn instead.
+   *
+   * Notice that these are not guaranteed to come in the same order as the
+   * instantiation lemmas above.
+   */
   void getInstantiationTermVectors(Expr q,
                                    std::vector<std::vector<Expr> >& tvecs);