mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

compiler warnings/bugs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-02 19:36:22 -08:00
parent 0d05104d8c
commit 39d2818923
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/solver/simplifier_solver.cpp
View file

@ -224,7 +224,7 @@ public:
}
proof_ref m_proof;
proof* get_proof_core() {
proof* get_proof_core() override {
proof* p = s->get_proof();
m_proof = p;
if (p) {
@ -271,7 +271,7 @@ public:
std::string reason_unknown() const override { return s->reason_unknown(); }
void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
void get_labels(svector<symbol>& r) override { s->get_labels(r); }
void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); }
void get_unsat_core(expr_ref_vector& r) override { s->get_unsat_core(r); replace(r); }
ast_manager& get_manager() const override { return s->get_manager(); }
void reset_params(params_ref const& p) override { s->reset_params(p); }
params_ref const& get_params() const override { return s->get_params(); }
@ -313,7 +313,7 @@ public:
clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset));
offset += c.size();
}
return check_sat_cc(cube1, clauses1);
return s->check_sat_cc(cube1, clauses1);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {