mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
00d35c2777
commit
8dde1bf86d
|
@ -386,12 +386,6 @@ namespace {
|
|||
//
|
||||
// ------------------------------------
|
||||
|
||||
inline enode * get_enode(context & ctx, app * n) {
|
||||
SASSERT(ctx.e_internalized(n));
|
||||
enode * e = ctx.get_enode(n);
|
||||
SASSERT(e);
|
||||
return e;
|
||||
}
|
||||
inline enode * mk_enode(context & ctx, quantifier * qa, app * n) {
|
||||
ctx.internalize(n, false, ctx.get_generation(qa));
|
||||
enode * e = ctx.get_enode(n);
|
||||
|
@ -446,6 +440,13 @@ namespace {
|
|||
}
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
inline enode * get_enode(context & ctx, app * n) const {
|
||||
SASSERT(ctx.e_internalized(n));
|
||||
enode * e = ctx.get_enode(n);
|
||||
SASSERT(e);
|
||||
return e;
|
||||
}
|
||||
|
||||
void display_label_hashes_core(std::ostream & out, app * p) const {
|
||||
if (p->is_ground()) {
|
||||
enode * e = get_enode(*m_context, p);
|
||||
|
@ -587,7 +588,7 @@ namespace {
|
|||
}
|
||||
};
|
||||
|
||||
inline std::ostream & operator<<(std::ostream & out, code_tree const & tree) {
|
||||
std::ostream & operator<<(std::ostream & out, code_tree const & tree) {
|
||||
tree.display(out);
|
||||
return out;
|
||||
}
|
||||
|
|
|
@ -622,6 +622,7 @@ namespace smt {
|
|||
void assign_eh(quantifier * q) override {
|
||||
m_active = true;
|
||||
ast_manager& m = m_context->get_manager();
|
||||
(void)m;
|
||||
if (!m_fparams->m_ematching) {
|
||||
return;
|
||||
}
|
||||
|
|
|
@ -34,8 +34,8 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m):
|
|||
m_new_args(m),
|
||||
m_rewrite_todo(m),
|
||||
m_rewrite_cache(m),
|
||||
m_new_exprs(m),
|
||||
m_in_processed(m) {
|
||||
m_in_processed(m),
|
||||
m_new_exprs(m) {
|
||||
params_ref p;
|
||||
p.set_bool("elim_and", true);
|
||||
m_bsimp.updt_params(p);
|
||||
|
|
Loading…
Reference in a new issue