From 8118292def44c9cf75f67920808cb6270dc3943f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 23:20:44 -0700 Subject: [PATCH] fix #3754 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_fpa.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index e103c8242..df3914cfb 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -481,7 +481,8 @@ namespace smt { case OP_FPA_TO_IEEE_BV: { expr_ref conv(m); conv = convert(term); - assert_cnstr(m.mk_eq(term, conv)); + expr_ref eq(m.mk_eq(term, conv), m); + assert_cnstr(eq); assert_cnstr(mk_side_conditions()); break; }