From 8e69f76784a6fb6ef9418dfdf0d2c1aca11fb9b7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 13:27:32 +0000 Subject: [PATCH] Add additional equality in theory_fpa --- src/smt/theory_fpa.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 1543ac2c29a..c36346de400 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -454,13 +454,9 @@ namespace smt { expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) }; cc_args = m_bv_util.mk_concat(3, args); c = m.mk_eq(wrapped, cc_args); - // NB code review: #5454 exposes a bug in fpa_solver that - // could be latent here as well. It needs also the equality - // n == bv_val_e to be asserted such that whenever something is assigned th - // bit-vector value cc_args it is equated with n - // I don't see another way this constraint would be enforced. assert_cnstr(c); assert_cnstr(mk_side_conditions()); + assert_cnstr(m.mk_eq(n, bv_val_e)); } else { expr_ref wu(m);