From 7c12ab47165a88ab514c8cddcf65b1be6e784ec8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 May 2013 14:40:57 -0700 Subject: [PATCH] fix some compiler warnings Signed-off-by: Nikolaj Bjorner --- src/muz_qe/aig_exporter.cpp | 2 ++ src/muz_qe/clp_context.cpp | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) 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);