mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

#4889 avoid double internalize of bvle

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-20 09:09:28 -08:00
parent b38b6daba3
commit 1e463955c2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_bv.cpp
View file

@ -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);