From 8491b3bebe2fb756e257b96dae14c9a0ae68dbc1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 31 Oct 2015 18:51:32 +0000 Subject: [PATCH] Revert "Fixed use of mk_th_axiom in theory_fpa." This reverts commit 89e99c7b4b1b4d75d016e53bee434d9b4cff6939. --- src/smt/theory_fpa.cpp | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 15caae296..7b8a83520 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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; }