mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

Fixed use of mk_th_axiom in theory_fpa.

Browse source 
Relates to #227
This commit is contained in:
Christoph M. Wintersteiger 2015-10-31 13:57:17 +00:00
parent 2bd2dd3334
commit 89e99c7b4b
1 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_fpa.cpp
View file

@ -560,7 +560,21 @@ namespace smt {
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
bv_atom = m.mk_and(bv_atom, mk_side_conditions()); bv_atom = m.mk_and(bv_atom, mk_side_conditions());
assert_cnstr(m.mk_iff(atom, bv_atom)); // CMW: Do not use assert_cnstr here; the internalizer expects normalized expressions.
// See GitHub issue #227
// assert_cnstr(m.mk_iff(atom, bv_atom));
ctx.internalize(atom, false);
ctx.internalize(bv_atom, false);
literal lit1(ctx.get_literal(atom));
literal lit2(ctx.get_literal(bv_atom));
ctx.mark_as_relevant(lit1);
ctx.mark_as_relevant(lit2);
literal lits1[2] = { lit1, ~lit2 };
literal lits2[2] = { ~lit1, lit2 };
ctx.mk_th_axiom(get_id(), 2, lits1);
ctx.mk_th_axiom(get_id(), 2, lits2);
return true; return true;
} }