diff --git a/doc/options.rst b/doc/options.rst
index 873bfeef1bb8dfff0341a2a1a5aefa3cc30e8f81..f55fa74fe47e980cc9fb964a2884461d0d7527b5 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -144,8 +144,16 @@ These options are available by all Leon components:
   
   * ``smt-z3-q``
    
-    Z3 through SMT-LIB, but (recursive) functions are encoded with universal
-    quantification, and inductive reasoning happens within the solver.
+    Z3 through SMT-LIB, but (recursive) functions are not unrolled and are 
+    instead encoded with universal quantification.
+    For example, ``def foo(x:A) = e`` would be encoded by asserting
+    
+    .. math::
+    
+      \forall (x:A). foo(x) = e
+
+    even if ``e`` contains an invocation to ``foo``.
+
     Currently, this solver does not handle higher-order functions.
   
   * ``unrollz3``