From 89e99c7b4b1b4d75d016e53bee434d9b4cff6939 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 31 Oct 2015 13:57:17 +0000 Subject: [PATCH] Fixed use of mk_th_axiom in theory_fpa. Relates to #227 --- src/smt/theory_fpa.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7b8a83520..15caae296 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -560,7 +560,21 @@ namespace smt { 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)); + // 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; }