fix #4836

Z3Prover · Nov 30, 2020 · bb24b3f · bb24b3f
1 parent 260f759
commit bb24b3f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
@@ -409,6 +409,7 @@ class bv_util : public bv_recognizers {
         return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n);
     }
     app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args);  }
+    app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.c_ptr());  }
     app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args);  }
     app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args);  }
     app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args);  }

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
@@ -1252,8 +1252,11 @@ namespace smt {
                 TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
                 TRACE("bv", tout << bit << " -> " << bit2 << " " << val << " -> " << val2 << " " << ctx.get_scope_level() << "\n";);
 
-                SASSERT(bit != ~bit2);
-
+                if (bit == ~bit2) {
+                    add_new_diseq_axiom(v, v2, idx);
+                    return;
+                }
+
                 if (val != val2) {
                     literal consequent = bit2;
                     if (val == l_false) {