From 1e463955c20eba19026941b439e295c4e74e0375 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Feb 2022 09:09:28 -0800 Subject: [PATCH] #4889 avoid double internalize of bvle Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index ba0c2933c..6c6904c39 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -993,7 +993,9 @@ namespace smt { process_args(n); expr_ref_vector arg1_bits(m), arg2_bits(m); get_arg_bits(n, 0, arg1_bits); - get_arg_bits(n, 1, arg2_bits); + get_arg_bits(n, 1, arg2_bits); + if (ctx.b_internalized(n)) + return; expr_ref le(m); if (Signed) m_bb.mk_sle(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le);