From 336fa6ae8302e93ea9c72703a0949ce51e8b65b1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 1 Sep 2015 17:52:19 +0100 Subject: [PATCH] Bugfix for FP to BV conversion of UFs --- src/ast/fpa/fpa2bv_rewriter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 6ea6b402f..b77026eae 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -176,7 +176,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } } - if (f->get_family_id() != m_conv.fu().get_family_id()) + if (f->get_family_id() != 0 && f->get_family_id() != m_conv.fu().get_family_id()) { bool is_float_uf = m_conv.is_float(f->get_range()); unsigned i = 0;