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

src/muz/pdr/pdr_sym_mux.h

@@ -93,7 +93,6 @@ private:
     std::string get_suffix(unsigned i);
     void ensure_tuple_size(func_decl * prim, unsigned sz);
 
-    expr_ref isolate_o_idx(expr* e, unsigned idx) const;
 public:
     sym_mux(ast_manager & m);
 
@@ -241,8 +240,6 @@ public:
     func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); }
     func_decl * const * end_prim_preds() const { return m_prim_preds.end(); }
 
-    void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const;
-
     std::string pp_model(const model_core & mdl) const;
 };
 }

src/opt/opt_context.cpp

@@ -896,7 +896,7 @@ namespace opt {
                 }
                 mk_atomic(terms);
                 SASSERT(obj.m_id == id);
-                obj.m_term = to_app(orig_term);
+                obj.m_term = orig_term?to_app(orig_term):0;
                 obj.m_terms.reset();
                 obj.m_terms.append(terms);
                 obj.m_weights.reset();
@@ -940,6 +940,9 @@ namespace opt {
     bool context::verify_model(unsigned index, model* md, rational const& _v) {
         rational r;
         app_ref term = m_objectives[index].m_term;
+        if (!term) {
+            return true;
+        }
         rational v = m_objectives[index].m_adjust_value(_v);
         expr_ref val(m);
         model_ref mdl = md;

src/opt/opt_context.h

@@ -226,8 +226,6 @@ namespace opt {
         virtual bool verify_model(unsigned id, model* mdl, rational const& v);
 
     private:
-        void validate_feasibility(maxsmt& ms);
-
         lbool execute(objective const& obj, bool committed, bool scoped);
         lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
         lbool execute_maxsat(symbol const& s, bool committed, bool scoped);

src/smt/asserted_formulas.h

@@ -106,7 +106,6 @@ public:
     void assert_expr(expr * e, proof * in_pr);
     void assert_expr(expr * e);
     void reset();
-    void set_cancel_flag(bool f);
     void push_scope();
     void pop_scope(unsigned num_scopes);
     bool inconsistent() const { return m_inconsistent; }

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -35,9 +35,9 @@ Notes:
 tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
 
     params_ref solve_eq_p;
-    // conservative guassian elimination. 
-    solve_eq_p.set_uint("solve_eqs_max_occs", 2); 
-    
+    // conservative guassian elimination.
+    solve_eq_p.set_uint("solve_eqs_max_occs", 2);
+
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
     simp2_p.set_bool("pull_cheap_ite", true);
@@ -61,13 +61,13 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
             using_params(mk_simplify_tactic(m), simp2_p),
             //
             // Z3 can solve a couple of extra benchmarks by using hoist_mul
-            // but the timeout in SMT-COMP is too small. 
+            // but the timeout in SMT-COMP is too small.
             // Moreover, it impacted negatively some easy benchmarks.
             // We should decide later, if we keep it or not.
             //
             using_params(mk_simplify_tactic(m), hoist_p),
             mk_max_bv_sharing_tactic(m),
-            mk_ackermannize_bv_tactic(m,p)
+            if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
             );
 }
 
@@ -80,14 +80,14 @@ static tactic * main_p(tactic* t) {
 }
 
 
-tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {    
+tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
 
     params_ref local_ctx_p = p;
     local_ctx_p.set_bool("local_ctx", true);
 
     params_ref solver_p;
     solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
-    
+
     params_ref no_flat_p;
     no_flat_p.set_bool("flat", false);
 
@@ -98,7 +98,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
 
     params_ref big_aig_p;
     big_aig_p.set_bool("aig_per_assertion", false);
-    
+
     tactic* preamble_st = mk_qfbv_preamble(m, p);
     tactic * st = main_p(and_then(preamble_st,
                                   // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
@@ -119,10 +119,10 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
                                                                                                   big_aig_p))))),
                                                      sat),
                                             smt))));
-    
+
     st->updt_params(p);
     return st;
-    
+
 }
 
 
@@ -131,9 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
     tactic * new_sat = cond(mk_produce_proofs_probe(),
                             and_then(mk_simplify_tactic(m), mk_smt_tactic()),
                             mk_sat_tactic(m));
-    
+
     return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
 
 }
-
-

src/util/small_object_allocator.cpp

@@ -77,7 +77,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
     SASSERT(m_alloc_size >= size);
     SASSERT(p);
     m_alloc_size -= size;
-    if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
         memory::deallocate(p);
         return;
     }
@@ -96,7 +96,7 @@ void * small_object_allocator::allocate(size_t size) {
     return memory::allocate(size);
 #endif
     m_alloc_size += size;
-    if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
         return memory::allocate(size);
 #ifdef Z3DEBUG
     size_t osize = size;