diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 560ee5885..98722022c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include #include +#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 75d9aa604..94f282265 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -66,7 +66,7 @@ Revision History: namespace stl_ext { template <> class hash { - stl_ext::hash H; + stl_ext::hash H; public: size_t operator()(const std::string &s) const { return H(s.c_str()); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f35dae93f..b85df81be 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -172,7 +172,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ std::vector names; - std::vector types; + std::vector types; std::vector bound_asts; unsigned num_bound = bvs.size(); @@ -485,7 +485,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ get_farkas_coeffs(proof,rats); coeffs.resize(rats.size()); for(unsigned i = 0; i < rats.size(); i++){ - sort *is = m().mk_sort(m_arith_fid, INT_SORT); + class sort *is = m().mk_sort(m_arith_fid, INT_SORT); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); coeffs[i] = coeff; } diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 645c72ccb..7da247287 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -22,6 +22,7 @@ Revision History: #include +#include #include "iz3hash.h" #include"well_sorted.h" diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index df6fcaf53..31b375c0f 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -58,20 +58,20 @@ namespace stl_ext { class free_func_visitor { ast_manager& m; func_decl_set m_funcs; - obj_hashtable m_sorts; + obj_hashtable m_sorts; public: free_func_visitor(ast_manager& m): m(m) {} void operator()(var * n) { } void operator()(app * n) { m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); + class sort* s = m.get_sort(n); if (s->get_family_id() == null_family_id) { m_sorts.insert(s); } } void operator()(quantifier * n) { } func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } + obj_hashtable& sorts() { return m_sorts; } }; class iz3pp_helper : public iz3mgr { @@ -146,8 +146,8 @@ void iz3pp(ast_manager &m, func_decl_set &funcs = visitor.funcs(); func_decl_set::iterator it = funcs.begin(), end = funcs.end(); - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); + obj_hashtable& sorts = visitor.sorts(); + obj_hashtable::iterator sit = sorts.begin(), send = sorts.end();