From 5121017f197260e32bec9aa268975ba6677936d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Oct 2020 13:19:24 -0700 Subject: [PATCH] build warnings from #4727 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/fpa_solver.h | 2 +- src/sat/smt/q_model_finder.cpp | 2 +- src/sat/smt/q_model_fixer.h | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h index f09a1dd8c..386da39ac 100644 --- a/src/sat/smt/fpa_solver.h +++ b/src/sat/smt/fpa_solver.h @@ -71,7 +71,7 @@ namespace fpa { void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); } sat::check_result check() override { return sat::check_result::CR_DONE; } - euf::th_solver* clone(sat::solver*, euf::solver& ctx) { return alloc(solver, ctx); } + euf::th_solver* clone(sat::solver*, euf::solver& ctx) override { return alloc(solver, ctx); } }; diff --git a/src/sat/smt/q_model_finder.cpp b/src/sat/smt/q_model_finder.cpp index 3777709f5..6077aaaa9 100644 --- a/src/sat/smt/q_model_finder.cpp +++ b/src/sat/smt/q_model_finder.cpp @@ -25,7 +25,7 @@ Notes: namespace q { - model_finder::model_finder(euf::solver&): + model_finder::model_finder(euf::solver& ctx): ctx(ctx), m(ctx.get_manager()) {} expr_ref model_finder::inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation) { diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index 73962e684..d14e5b351 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -94,7 +94,7 @@ namespace q { */ void operator()(model& mdl); - quantifier_macro_info* operator()(quantifier* q); + quantifier_macro_info* operator()(quantifier* q) override; projection_meta_data* operator()(func_decl* f, unsigned idx) const { projection_meta_data* r = nullptr;