mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Bugfix for theory_fpa

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-02 19:08:52 +00:00
parent fb0999b3cf
commit ba70ab9ad2
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_fpa.cpp
View file

@ -737,10 +737,11 @@ namespace smt {
expr_ref converted(m);
converted = m.mk_and(convert(e), mk_side_conditions());
if (is_true)
assert_cnstr(m.mk_implies(e, converted));
else
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
expr_ref cnstr(m);
cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted));
m_th_rw(cnstr);
assert_cnstr(cnstr);
}
void theory_fpa::relevant_eh(app * n) {