3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 03:46:17 +00:00

address other warnings per input from delcypher

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-10 17:23:59 +01:00
parent 6594c3a046
commit 32c63ce4cd
3 changed files with 3 additions and 1 deletions

View file

@ -111,7 +111,7 @@ protected:
void elim_reflex_prs(unsigned spos); void elim_reflex_prs(unsigned spos);
public: public:
rewriter_core(ast_manager & m, bool proof_gen); rewriter_core(ast_manager & m, bool proof_gen);
~rewriter_core(); virtual ~rewriter_core();
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
void reset(); void reset();
void cleanup(); void cleanup();

View file

@ -72,6 +72,7 @@ public:
// m_params.set_func_decl(m_last, f); // m_params.set_func_decl(m_last, f);
// m_last = symbol::null; // m_last = symbol::null;
} }
virtual void set_next_arg(cmd_context & ctx, sexpr * n) { UNREACHABLE(); }
}; };
#endif #endif

View file

@ -871,6 +871,7 @@ namespace datalog {
class table_row_mutator_fn { class table_row_mutator_fn {
public: public:
virtual ~table_row_mutator_fn() {}
/** /**
\brief The function is called for a particular table row. The \c func_columns contains \brief The function is called for a particular table row. The \c func_columns contains
a pointer to an array of functional column values that can be modified. If the function a pointer to an array of functional column values that can be modified. If the function