From 7fb30c38aebbf8d956c02a37a9f944f140d97c0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 May 2016 12:49:07 -0700 Subject: [PATCH] disallow illegal use per #604 Signed-off-by: Nikolaj Bjorner --- src/muz/fp/dl_cmds.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 2a6ff04d4..874d14538 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -219,6 +219,13 @@ public: virtual void set_next_arg(cmd_context & ctx, func_decl* t) { m_target = t; + if (t->get_family_id() != null_family_id) { + throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted"); + } + datalog::context& dlctx = m_dl_ctx->dlctx(); + if (!dlctx.get_predicates().contains(t)) { + throw cmd_exception("Invalid query argument, expected a predicate registered as a relation"); + } } virtual void prepare(cmd_context & ctx) {