mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
build warnings from #4727
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
49dfaeb406
commit
5121017f19
|
@ -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); }
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -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) {
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue