Merge branch 'master' of https://github.com/z3prover/z3

scripts/mk_util.py

@@ -889,7 +889,7 @@ def is_CXX_gpp():
     return is_compiler(CXX, 'g++')
 
 def is_clang_in_gpp_form(cc):
-    version_string = check_output([cc, '--version'])
+    version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8')
     return version_string.find('clang') != -1
 
 def is_CXX_clangpp():

src/ast/fpa/fpa2bv_converter.cpp

@@ -4085,7 +4085,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
-void fpa2bv_converter::reset(void) {
+void fpa2bv_converter::reset() {
     dec_ref_map_key_values(m, m_const2bv);
     dec_ref_map_key_values(m, m_rm_const2bv);
     dec_ref_map_key_values(m, m_uf2bvuf);

src/ast/fpa/fpa2bv_converter.h

@@ -150,7 +150,7 @@ public:
     void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
 
-    void reset(void);
+    void reset();
 
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;

src/ast/fpa_decl_plugin.cpp

@@ -160,7 +160,7 @@ bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) {
         return true;
     }
 
-    return 0;
+    return false;
 }
 
 bool fpa_decl_plugin::is_rm_numeral(expr * n) {

src/ast/macros/quasi_macros.cpp

@@ -91,7 +91,7 @@ public:
     void operator()(var * n) { m_bitset.set(n->get_idx(), true); }
     void operator()(quantifier * n) {}
     void operator()(app * n) {}
-    bool all_used(void) {
+    bool all_used() {
         for (unsigned i = 0; i < m_bitset.size() ; i++)
             if (!m_bitset.get(i))
                 return false;

src/smt/smt_context.h

@@ -1387,7 +1387,7 @@ namespace smt {
         void flush();
         config_mode get_config_mode(bool use_static_features) const;
         virtual void setup_context(bool use_static_features);
-        void setup_components(void);
+        void setup_components();
         void pop_to_base_lvl();
         void pop_to_search_lvl();
 #ifdef Z3DEBUG

src/tactic/arith/nla2bv_tactic.cpp

@@ -459,7 +459,7 @@ public:
         SASSERT(g->is_well_sorted());
     }
     
-    void cleanup(void) override {
+    void cleanup() override {
     }
 };
 

src/tactic/sls/bvsls_opt_engine.h

@@ -65,7 +65,7 @@ protected:
                        unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
                        mpz const & max_score, expr * objective);
 
-    mpz top_score(void) {
+    mpz top_score() {
         mpz res(0);
         obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
         for (obj_hashtable<expr>::iterator it = top_exprs.begin();

src/tactic/sls/sls_engine.h

@@ -99,7 +99,7 @@ public:
 
     // stats const & get_stats(void) { return m_stats; }
     void collect_statistics(statistics & st) const;
-    void reset_statistics(void) { m_stats.reset(); }    
+    void reset_statistics() { m_stats.reset(); }
 
     bool full_eval(model & mdl);
 
@@ -109,7 +109,7 @@ public:
     void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
     void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);            
 
-    lbool search(void);    
+    lbool search();
 
     lbool operator()();
     void operator()(goal_ref const & g, model_converter_ref & mc);

src/tactic/tactical.cpp

@@ -907,7 +907,7 @@ public:
         m_t->operator()(in, result, mc, pc, core);
     }
    
-    void cleanup(void) override { m_t->cleanup(); }
+    void cleanup() override { m_t->cleanup(); }
     void collect_statistics(statistics & st) const override { m_t->collect_statistics(st); }
     void reset_statistics() override { m_t->reset_statistics(); }
     void updt_params(params_ref const & p) override { m_t->updt_params(p); }

src/tactic/ufbv/ufbv_rewriter.cpp

@@ -196,14 +196,14 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
 class max_var_id_proc {
     unsigned    m_max_var_id;
 public:
-    max_var_id_proc(void):m_max_var_id(0) {}
+    max_var_id_proc():m_max_var_id(0) {}
     void operator()(var * n) {
         if(n->get_idx() > m_max_var_id)
             m_max_var_id = n->get_idx();
     }
     void operator()(quantifier * n) {}
     void operator()(app * n) {}
-    unsigned get_max(void) { return m_max_var_id; }
+    unsigned get_max() { return m_max_var_id; }
 };
 
 unsigned ufbv_rewriter::max_var_id(expr * e)
@@ -253,7 +253,7 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
     }
 }
 
-bool ufbv_rewriter::check_fwd_idx_consistency(void) {
+bool ufbv_rewriter::check_fwd_idx_consistency() {
     for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
         quantifier_set * set = it->m_value;
         SASSERT(set);

src/tactic/ufbv/ufbv_rewriter.h

@@ -173,7 +173,7 @@ class ufbv_rewriter {
     
     void insert_fwd_idx(expr * large, expr * small, quantifier * demodulator);
     void remove_fwd_idx(func_decl * f, quantifier * demodulator);
-    bool check_fwd_idx_consistency(void);
+    bool check_fwd_idx_consistency();
     void show_fwd_idx(std::ostream & out);
     bool is_demodulator(expr * e, expr_ref & large, expr_ref & small) const;
     bool can_rewrite(expr * n, expr * lhs);

src/util/hashtable.h

@@ -449,7 +449,7 @@ public:
             INSERT_LOOP_CORE_BODY();
         }
         UNREACHABLE();
-        return 0;
+        return false;
     }
 
     bool insert_if_not_there_core(const data & e, entry * & et) {

src/util/mpf.h

@@ -190,8 +190,8 @@ public:
     void mk_pinf(unsigned ebits, unsigned sbits, mpf & o);
     void mk_ninf(unsigned ebits, unsigned sbits, mpf & o);
 
-    unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; }
-    unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; }
+    unsynch_mpz_manager & mpz_manager() { return m_mpz_manager; }
+    unsynch_mpq_manager & mpq_manager() { return m_mpq_manager; }
 
     unsigned hash(mpf const & a) {
         return hash_u_u(m_mpz_manager.hash(a.significand),