diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 74c909c02..a90d420cb 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -188,9 +188,8 @@ namespace datalog { if (m_trail.get_num_scopes() == 0) { throw default_exception("there are no backtracking points to pop to"); } - if(m_engine.get()){ - if(get_engine() != DUALITY_ENGINE) - throw default_exception("operation is not supported by engine"); + if (m_engine.get() && get_engine() != DUALITY_ENGINE) { + throw default_exception("pop operation is only supported by duality engine"); } m_trail.pop_scope(1); } diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 874d14538..e8e93dafc 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -229,6 +229,7 @@ public: } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. parametric_cmd::prepare(ctx); m_target = 0; } @@ -390,6 +391,7 @@ public: virtual unsigned get_arity() const { return VAR_ARITY; } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. m_arg_idx = 0; m_query_arg_idx = 0; m_domain = 0; @@ -450,6 +452,7 @@ public: virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. m_arg_idx = 0; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {