diff --git a/interpreter/src/shell/qepcad-inter/qepcad-inter.h b/interpreter/src/shell/qepcad-inter/qepcad-inter.h
index 71c9fcc2e..bacd7f809 100755
--- a/interpreter/src/shell/qepcad-inter/qepcad-inter.h
+++ b/interpreter/src/shell/qepcad-inter/qepcad-inter.h
@@ -95,6 +95,9 @@ class CommQepcadSat : public EICommand
       else return new ErrObj("Symbol not understood");
     }
     // TODO!! check that F is quantifier free
+    if (!isQuantifierFree(F)) {
+      return new ErrObj("Input has quantifiers: 'qepcad-sat' requires a quantifier-free formula.  Try 'qepcad-qe'.  See (help 'qepcad-sat).");
+    }
     TAndRef Fp = new TAndObj();
     Fp->AND(F);
     bool conjunctionCase = isConjunctionOfAtoms(Fp);