#5223

src/ast/rewriter/bit_blaster/bit_blaster.h

@@ -59,6 +59,7 @@ class bit_blaster : public bit_blaster_tpl<bit_blaster_cfg> {
 public:
     bit_blaster(ast_manager & m, bit_blaster_params const & params);
     bit_blaster_params const & get_params() const { return this->m_params; }
+    void set_flat(bool f) { m_rw.set_flat(f); }
 };
 
 

src/sat/sat_solver.cpp

@@ -1029,7 +1029,7 @@ namespace sat {
                     return false;
             } while (m_qhead < m_trail.size());
 
-            if (m_ext && !is_probing()) 
+            if (m_ext && (!is_probing() || at_base_lvl())) 
                 m_ext->unit_propagate();            
         }
         if (m_inconsistent)

src/sat/smt/array_axioms.cpp

@@ -174,9 +174,13 @@ namespace array {
         SASSERT(store->get_num_args() == 1 + select->get_num_args());
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
+
+        if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
+            return false;
+
         sel1_args.push_back(store);
         sel2_args.push_back(store->get_arg(0));
-
+        
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
             has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
@@ -191,6 +195,7 @@ namespace array {
         expr_ref sel1(a.mk_select(sel1_args), m);
         expr_ref sel2(a.mk_select(sel2_args), m);
         expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m);
+
         euf::enode* s1 = e_internalize(sel1);
         euf::enode* s2 = e_internalize(sel2);
         TRACE("array", 
@@ -200,9 +205,13 @@ namespace array {
         if (s1->get_root() == s2->get_root())
             return false;
 
-        sat::literal sel_eq = mk_literal(sel_eq_e);
-        if (s().value(sel_eq) == l_true)
-            return false;
+        sat::literal sel_eq = sat::null_literal;
+        auto init_sel_eq = [&]() {
+            if (sel_eq != sat::null_literal) 
+                return true;
+            sel_eq = mk_literal(sel_eq_e);
+            return s().value(sel_eq) != l_true;
+        };
 
         bool new_prop = false;
         for (unsigned i = 1; i < num_args; i++) {
@@ -213,11 +222,17 @@ namespace array {
             if (r1 == r2)
                 continue;
             if (m.are_distinct(r1->get_expr(), r2->get_expr())) {
-                new_prop = true;
-                add_clause(sel_eq);
+                if (init_sel_eq() && add_clause(sel_eq))
+                    new_prop = true;
                 break;
             }
             sat::literal idx_eq = eq_internalize(idx1, idx2);
+            if (s().value(idx_eq) == l_true)
+                continue;
+            if (s().value(idx_eq) == l_undef)
+                new_prop = true;
+            if (!init_sel_eq())
+                break;
             if (add_clause(idx_eq, sel_eq))
                 new_prop = true;
         }

src/sat/smt/bv_solver.cpp

@@ -55,6 +55,7 @@ namespace bv {
         m_ackerman(*this),
         m_bb(m, get_config()),
         m_find(*this) {
+        m_bb.set_flat(false);
     }
 
     void solver::fixed_var_eh(theory_var v1) {

src/sat/smt/euf_model.cpp

@@ -253,13 +253,14 @@ namespace euf {
             if (!is_relevant(n))
                 continue;
             bool tt = l_true == s().value(n->bool_var());
-            if (tt && mdl.is_false(e)) {
-                IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n");
-                for (auto* arg : euf::enode_args(n))
-                    IF_VERBOSE(0, verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n");
-            }
-            if (!tt && mdl.is_true(e))
-                IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n");
+            if (tt && !mdl.is_false(e))
+                continue;
+            if (!tt && !mdl.is_true(e))
+                continue;
+            IF_VERBOSE(0, 
+                       verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
+                       for (auto* arg : euf::enode_args(n))
+                           verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
         }
 
     }