mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 21:49:29 +00:00
Code Activity

Bugfix for FP UFs.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-08 12:45:26 +01:00
parent a2503af585
commit c787ea1a3b
2 changed files with 23 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/fpa/fpa2bv_converter.h
View file

@ -68,7 +68,7 @@ public:
bool is_float(sort * s) { return m_util.is_float(s); }
bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
bool is_rm(expr * e) { return m_util.is_rm(e); }
bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
bool is_rm(sort * s) { return m_util.is_rm(s); }
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }