mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
cb8603177e
commit
039de6a2c8
|
@ -34,7 +34,7 @@ namespace euf {
|
|||
public:
|
||||
basic_extract_eq(ast_manager& m) : m(m) {}
|
||||
|
||||
virtual void set_allow_booleans(bool f) {
|
||||
void set_allow_booleans(bool f) override {
|
||||
m_allow_bool = f;
|
||||
}
|
||||
|
||||
|
@ -74,7 +74,7 @@ namespace euf {
|
|||
eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(m.mk_false(), m), d));
|
||||
}
|
||||
|
||||
void updt_params(params_ref const& p) {
|
||||
void updt_params(params_ref const& p) override {
|
||||
tactic_params tp(p);
|
||||
m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
|
||||
}
|
||||
|
@ -263,7 +263,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
|
||||
void updt_params(params_ref const& p) {
|
||||
void updt_params(params_ref const& p) override {
|
||||
tactic_params tp(p);
|
||||
m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver());
|
||||
}
|
||||
|
|
|
@ -49,7 +49,7 @@ class model_reconstruction_trail {
|
|||
entry(ast_manager& m, func_decl* h) : m_decl(h, m), m_def(m), m_dep(m) {}
|
||||
|
||||
entry(ast_manager& m, func_decl* f, expr* def, expr_dependency* dep, vector<dependent_expr> const& rem) :
|
||||
m_decl(f, m), m_def(def, m), m_removed(rem), m_dep(dep, m) {}
|
||||
m_removed(rem), m_decl(f, m), m_def(def, m), m_dep(dep, m) {}
|
||||
|
||||
bool is_loose() const { return !m_removed.empty(); }
|
||||
|
||||
|
|
Loading…
Reference in a new issue