mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Fixed rewriter bug in theory_fpa.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-31 18:53:40 +00:00
parent 8491b3bebe
commit 1d7aa9ba2f
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_fpa.cpp
View file

@ -558,9 +558,10 @@ namespace smt {
expr_ref bv_atom(m);
bv_atom = convert_atom(atom);
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
bv_atom = m.mk_and(bv_atom, mk_side_conditions());
assert_cnstr(m.mk_iff(atom, bv_atom));
expr_ref constr(m);
constr = m.mk_iff(atom, m.mk_and(bv_atom, mk_side_conditions()));
m_th_rw(constr);
assert_cnstr(constr);
return true;
}