mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Revert "Fixed use of mk_th_axiom in theory_fpa."

Browse source 
This reverts commit 89e99c7b4b.
This commit is contained in:
Christoph M. Wintersteiger 2015-10-31 18:51:32 +00:00
parent 89e99c7b4b
commit 8491b3bebe
1 changed files with 1 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_fpa.cpp
View file

@ -560,21 +560,7 @@ namespace smt {
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
bv_atom = m.mk_and(bv_atom, mk_side_conditions());
// 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);
assert_cnstr(m.mk_iff(atom, bv_atom));
return true;
}