mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

initialize manager to avoid unrelated error message, issue #604

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-15 12:59:42 -07:00
parent 7fb30c38ae
commit e5ca676251
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/base/dl_context.cpp
View file

@ -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);
}

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

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