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);