diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 2d8e7be01..8a9304480 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -770,6 +770,9 @@ namespace qe {
             while (!vars.empty());
             SASSERT(m_vars.back().empty()); 
             initialize_levels();
+            if (has_uninterpreted(m, fml))
+                throw tactic_exception("formula contains uninterpreted functions");
+
             TRACE("qe", tout << fml << "\n";);
         }