#4889 avoid double internalize of bvle

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Feb 20, 2022 · 1e46395 · 1e46395
1 parent b38b6da
commit 1e46395
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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);