diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index df3059d4b..a8f4d74b7 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -137,7 +137,7 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
         if (!p.has_def(d)) {
-            std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
+            std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
             SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
             return;
         }
@@ -158,6 +158,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return;
         }
+        if (!pd.get_def()->get_cases().empty()) {
+            std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
+            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            return;            
+        }
+                
         if (abs_body->get_sort() != d->get_range()) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);            
             return;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index ce9de96d4..7514055c5 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1387,6 +1387,7 @@ inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->ge
 inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); }
 inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; }
 inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; }
+inline bool is_uninterp(func_decl const * n) { return n->get_family_id() == null_family_id; }
 inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; }
 inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); }
 inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); }
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index dcff35e82..8e1279c0a 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -203,8 +203,9 @@ namespace recfun {
             def const& get_def(func_decl* f) const { return *(m_defs[f]); }
             promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); }
             def& get_def(func_decl* f) { return *(m_defs[f]); }
-            bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); }
+            bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); }            
             case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); }
+            bool is_defined(func_decl* f) {return has_case_def(f) && !get_def(f).get_cases().empty(); }
 
             func_decl_ref_vector get_rec_funs() {
                 func_decl_ref_vector result(m());
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 4efe79dd3..c9d2c7797 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -644,6 +644,12 @@ namespace datalog {
     }
 
     void context::add_table_fact(func_decl * pred, const table_fact & fact) {
+        if (!is_uninterp(pred)) {
+            std::stringstream strm;
+            strm << "Predicate " << pred->get_name() << " when used for facts should be uninterpreted";        
+            throw default_exception(strm.str());
+        }
+        
         if (get_engine() == DATALOG_ENGINE) {
             ensure_engine();
             m_rel->add_fact(pred, fact);
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 24bfb3355..40e789204 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -166,7 +166,7 @@ namespace smt {
         unsigned num = get_num_bool_vars();
         for (unsigned v = 0; v < num; v++) {
             expr * n = m_bool_var2expr[v];
-            ast_def_ll_pp(out, m, n, get_pp_visited(), true, false);
+            ast_def_ll_pp(out << v << " ", m, n, get_pp_visited(), true, false);
         }
     }