mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix build, likely addressing issue #420

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-09 22:58:08 +00:00
parent a0503ba6a1
commit cacfa0cb98
2 changed files with 5 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/muz/pdr/pdr_manager.cpp
View file

@ -159,22 +159,17 @@ namespace pdr {
out << "(pop)\n";
}
}
vector<std::string> manager::get_state_suffixes() {
vector<std::string> res;
res.push_back("_n");
return res;
}
manager::manager(smt_params& fparams, unsigned max_num_contexts, ast_manager& manager) :
m(manager),
m_fparams(fparams),
m_brwr(m),
m_mux(m, get_state_suffixes()),
m_brwr(m),
m_mux(m, m_state_suffixes),
m_background(m.mk_true(), m),
m_contexts(fparams, max_num_contexts, m),
m_next_unique_num(0)
{
m_state_suffixes.push_back("_n");
}

5
src/muz/pdr/pdr_manager.h
View file

@ -81,6 +81,7 @@ namespace pdr {
mutable bool_rewriter m_brwr;
vector<std::string> m_state_suffixes;
sym_mux m_mux;
expr_ref m_background;
decl_vector m_o0_preds;
@ -89,9 +90,7 @@ namespace pdr {
/** whenever we need an unique number, we get this one and increase */
unsigned m_next_unique_num;
static vector<std::string> get_state_suffixes();
unsigned n_index() const { return 0; }
unsigned o_index(unsigned i) const { return i+1; }