diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp index 1d6ef3633..ca0030fc3 100755 --- a/src/muz_qe/aig_exporter.cpp +++ b/src/muz_qe/aig_exporter.cpp @@ -265,6 +265,8 @@ namespace datalog { case AST_VAR: return get_var(e); + default: + UNREACHABLE(); } UNREACHABLE(); diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp index 5dd6fb9d8..94a956eb9 100644 --- a/src/muz_qe/clp_context.cpp +++ b/src/muz_qe/clp_context.cpp @@ -66,8 +66,9 @@ namespace datalog { m_ctx.ensure_opened(); m_solver.reset(); m_goals.reset(); - func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules()); + rm.mk_query(query, m_ctx.get_rules()); m_ctx.apply_default_transformation(); + func_decl *head_decl = m_ctx.get_rules().get_output_predicate(); expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m); ground(head);