From 1209302fe6c2d5fc1205f4f7b2bb5880f801e5d5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 21 Jan 2015 15:34:21 +0000 Subject: [PATCH] Fixed integration issues Signed-off-by: Christoph M. Wintersteiger --- src/muz/duality/duality_dl_interface.cpp | 2 +- src/qe/nlarith_util.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 0ab9762b0..aa186bd0a 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -82,7 +82,7 @@ namespace Duality { if(rpfp) dealloc(rpfp); if(ls) - (ls); + dealloc(ls); } }; diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index fce54aaa4..c555b71f1 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -1492,11 +1492,11 @@ namespace nlarith { } fml = mk_and(equivs.size(), equivs.c_ptr()); } - void mk_pinf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { + void mk_plus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { plus_inf_subst sub(*this); mk_inf_sign(sub, literals, fml, new_atoms); } - void mk_ninf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { + void mk_minus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { minus_inf_subst sub(*this); mk_inf_sign(sub, literals, fml, new_atoms); } @@ -1704,10 +1704,10 @@ namespace nlarith { app_ref fml(m()); app_ref_vector new_atoms(m()); if (is_pos) { - mk_pinf_sign(literals, fml, new_atoms); + mk_plus_inf_sign(literals, fml, new_atoms); } else { - mk_ninf_sign(literals, fml, new_atoms); + mk_minus_inf_sign(literals, fml, new_atoms); } simple_branch* br = alloc(simple_branch, m(), fml); swap_atoms(br, literals.lits(), new_atoms);