mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

disallow illegal use per #604

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-15 12:49:07 -07:00
parent 10cdd527ca
commit 7fb30c38ae
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/muz/fp/dl_cmds.cpp
View file

@ -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) {