From bb24b3f2bec212931f4518d8b8ae771594f6e277 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Nov 2020 21:08:28 -0800 Subject: [PATCH] fix #4836 --- src/ast/bv_decl_plugin.h | 1 + src/smt/theory_bv.cpp | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 252a2d4585b..f8d2e9e7067 100644 --- 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 index 730ffa9329d..fd5df0192e8 100644 --- 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) {