mirror of
https://github.com/Z3Prover/z3
synced 2025-07-25 21:57:00 +00:00
fix build again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4bcf1bf2f6
commit
f52baf1e17
1 changed files with 2 additions and 1 deletions
|
@ -112,6 +112,7 @@ namespace smt {
|
||||||
};
|
};
|
||||||
|
|
||||||
class fpa_rm_value_proc : public model_value_proc {
|
class fpa_rm_value_proc : public model_value_proc {
|
||||||
|
theory_fpa & m_th;
|
||||||
ast_manager & m;
|
ast_manager & m;
|
||||||
fpa_util & m_fu;
|
fpa_util & m_fu;
|
||||||
bv_util & m_bu;
|
bv_util & m_bu;
|
||||||
|
@ -119,7 +120,7 @@ namespace smt {
|
||||||
|
|
||||||
public:
|
public:
|
||||||
fpa_rm_value_proc(theory_fpa * th) :
|
fpa_rm_value_proc(theory_fpa * th) :
|
||||||
m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
|
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) { (void) m_th; }
|
||||||
|
|
||||||
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue