diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index c9d2c7797..230a452df 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -577,6 +577,7 @@ namespace datalog {
             m_rule_properties.check_uninterpreted_free();
             m_rule_properties.check_nested_free();
             m_rule_properties.check_infinite_sorts();
+            m_rule_properties.check_background_free();
             break;
         case SPACER_ENGINE:
             m_rule_properties.collect(r);
@@ -584,6 +585,7 @@ namespace datalog {
             m_rule_properties.check_for_negated_predicates();
             m_rule_properties.check_uninterpreted_free();
             m_rule_properties.check_quantifier_free(exists_k);
+            m_rule_properties.check_background_free();
             break;
         case BMC_ENGINE:
             m_rule_properties.collect(r);
@@ -598,13 +600,16 @@ namespace datalog {
             m_rule_properties.collect(r);
             m_rule_properties.check_existential_tail();
             m_rule_properties.check_for_negated_predicates();
+            m_rule_properties.check_background_free();
             break;
         case CLP_ENGINE:
             m_rule_properties.collect(r);
             m_rule_properties.check_existential_tail();
             m_rule_properties.check_for_negated_predicates();
+            m_rule_properties.check_background_free();
             break;
         case DDNF_ENGINE:
+            m_rule_properties.check_background_free();
             break;
         case LAST_ENGINE:
         default:
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 7632a0c2f..239fa73b6 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -139,6 +139,12 @@ void rule_properties::check_nested_free() {
     }
 }
 
+void rule_properties::check_background_free() {
+    if (m_ctx.get_num_assertions() > 0)
+        throw default_exception("engine does not support background assertions");
+}
+
+
 void rule_properties::check_existential_tail() {
     ast_mark visited;
     ptr_vector<expr> todo, tocheck;
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index 896b1bb16..a7ef9a0de 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -68,6 +68,7 @@ namespace datalog {
         void check_for_negated_predicates();
         void check_nested_free();
         void check_infinite_sorts();
+        void check_background_free();
         bool is_monotone() { return m_is_monotone; }
         void operator()(var* n);
         void operator()(quantifier* n);