diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/AbstractConstant.java b/com.ibm.wala.core/src/com/ibm/wala/logic/AbstractConstant.java
index cc9c76866..e7b336f65 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/AbstractConstant.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/AbstractConstant.java
@@ -31,6 +31,10 @@ public abstract class AbstractConstant implements IConstant {
   public Collection<? extends IConstant> getConstants() {
     return Collections.singleton(this);
   }
+
+  public Collection<? extends ITerm> getAllTerms() {
+    return Collections.singleton(this);
+  }
   
 
   @Override
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java
index 361263563..3e87cfc2d 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java
@@ -103,10 +103,10 @@ public class BinaryFormula extends AbstractBinaryFormula {
     return result;
   }
   
-  public Collection<? extends ITerm> getTerms() {
+  public Collection<? extends ITerm> getAllTerms() {
     Collection<ITerm> result = HashSetFactory.make();
-    result.addAll(f1.getTerms());
-    result.addAll(f2.getTerms());
+    result.addAll(f1.getAllTerms());
+    result.addAll(f2.getAllTerms());
     return result;
   }
 
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java
index a4e794ddc..f7bba1144 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java
@@ -11,7 +11,6 @@
 package com.ibm.wala.logic;
 
 
-
 public class BooleanConstant extends AbstractConstant {
   
   public static final BooleanConstant TRUE = new BooleanConstant(true);
@@ -38,5 +37,5 @@ public class BooleanConstant extends AbstractConstant {
   public int hashCode() {
     return val ? 11 : 13;
   }
-  
+
 }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java
index bc2b2a535..50abb7ea5 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java
@@ -62,4 +62,8 @@ public class BooleanConstantFormula implements IMaxTerm {
     return 163 * c.hashCode();
   }
 
+  public Collection<? extends ITerm> getAllTerms() {
+    return Collections.singleton(c);
+  }
+
 }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
index 238205322..e942c19d7 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
@@ -48,10 +48,10 @@ public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
     return result;
   }
 
-  public Collection<? extends ITerm> getTerms() {
+  public Collection<? extends ITerm> getAllTerms() {
     Collection<ITerm> result = HashSetFactory.make();
     for (IFormula f : maxTerms) {
-      result.addAll(f.getTerms());
+      result.addAll(f.getAllTerms());
     }
     return result;
   }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
index 0b2622956..00e40a217 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
@@ -39,10 +39,10 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
     return result;
   }
 
-  public Collection<? extends ITerm> getTerms() {
+  public Collection<? extends ITerm> getAllTerms() {
     Collection<ITerm> result = HashSetFactory.make();
     for (IFormula f : clauses) {
-      result.addAll(f.getTerms());
+      result.addAll(f.getAllTerms());
     }
     return result;
   }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java b/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java
index 81926251b..f97f136bb 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java
@@ -143,4 +143,13 @@ public class FunctionTerm extends AbstractTerm {
       return false;
     return true;
   }
+
+  public Collection<? extends ITerm> getAllTerms() {
+    Collection<ITerm> result = HashSetFactory.make();
+    result.add(this);
+    for (ITerm t : parameters) {
+      result.addAll(t.getAllTerms());
+    }
+    return result;
+  }
 }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java
index 0b3506711..9ce528bee 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java
@@ -41,9 +41,9 @@ public interface IFormula {
   public Collection<? extends IConstant> getConstants();
   
   /**
-   * @return the terms that appear in this formula
+   * @return all terms that appear in this formula, including recursive descent on on-atomic terms
    */
-  public Collection<? extends ITerm> getTerms();
+  public Collection<? extends ITerm> getAllTerms();
   
   public String prettyPrint(ILogicDecorator d);
  
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java b/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java
index ed62c9b9f..83c54600a 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java
@@ -32,4 +32,9 @@ public interface ITerm {
   public String prettyPrint(ILogicDecorator d);
 
   public Collection<? extends IConstant> getConstants();
+
+  /**
+   * Collect all terms that appear in this term, including subterms if this is a function term
+   */
+  public Collection<? extends ITerm> getAllTerms();
 }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
index f7bc88811..d41fb5d6f 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java
@@ -83,8 +83,8 @@ public class NotFormula implements IFormula {
     return f.getConstants();
   }
 
-  public Collection<? extends ITerm> getTerms() {
-    return f.getTerms();
+  public Collection<? extends ITerm> getAllTerms() {
+    return f.getAllTerms();
   }
 
   @Override
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java
index 177830041..24623d9f4 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java
@@ -108,8 +108,8 @@ public class QuantifiedFormula implements IMaxTerm {
     return f.getConstants();
   }
 
-  public Collection<? extends ITerm> getTerms() {
-    return f.getTerms();
+  public Collection<? extends ITerm> getAllTerms() {
+    return f.getAllTerms();
   }
 
   @Override
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java
index 37c946cfe..73c8a08c4 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java
@@ -34,6 +34,15 @@ public class RelationFormula implements IMaxTerm {
   public List<ITerm> getTerms() {
     return terms;
   }
+  
+
+  public Collection<? extends ITerm> getAllTerms() {
+    Collection<ITerm> result = HashSetFactory.make();
+    for (ITerm t: terms) {
+      result.addAll(t.getAllTerms());
+    }
+    return result;
+  }
 
   private RelationFormula(final IRelation R, final List<ITerm> terms) throws IllegalArgumentException {
     super();
@@ -171,4 +180,5 @@ public class RelationFormula implements IMaxTerm {
     result.append(terms.get(1).prettyPrint(d));
     return result.toString();
   }
+
 }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
index 877862318..9f392d0a2 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
@@ -275,16 +275,16 @@ public class Simplifier {
         Variable bound = q.getBoundVar();
         IFormula body = q.getFormula();
         // this could be inefficient. find a better algorithm.
-        for (Variable free : f.getFreeVariables()) {
-          if (q.getFreeVariables().contains(free)) {
+        for (ITerm t : f.getAllTerms()) {
+          if (q.getFreeVariables().contains(t)) {
             Variable fresh = makeFresh(q, f);
             IFormula testBody = substitute(body, bound, fresh);
-            IFormula testF = substitute(f, free, fresh);
+            IFormula testF = substitute(f, t, fresh);
             if (implies(testBody,testF)) {
               return true;
             }
           } else {
-            IFormula testBody = substitute(body, bound, free);
+            IFormula testBody = substitute(body, bound, t);
             if (implies(testBody, f)) {
               return true;
             }
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java
index 9f25296fd..9e36f3e1e 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java
@@ -93,4 +93,8 @@ public class Variable extends AbstractTerm implements Comparable<Variable> {
   public int compareTo(Variable o) throws NullPointerException {
     return this.getNumber() - o.getNumber();
   }
+
+  public Collection<? extends ITerm> getAllTerms() {
+    return Collections.singleton(this);
+  }
 }