diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp
index b02a286ab8e..54a3458add5 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp
@@ -55,8 +55,7 @@ void dfcc_is_freeablet::rewrite_calls(
             .set_identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE));
           target->call_arguments().push_back(write_set);
         }
-
-        if(fun_name == CPROVER_PREFIX "was_freed")
+        else if(fun_name == CPROVER_PREFIX "was_freed")
         {
           // insert call to precondition for vacuity checking
           auto inst = goto_programt::make_function_call(
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index 91ba47ecc1b..ec48935efb4 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -454,8 +454,7 @@ void dfcc_libraryt::fix_malloc_free_calls()
 
           if(fun_name == (CONTRACTS_PREFIX "malloc"))
             to_symbol_expr(ins->call_function()).set_identifier("malloc");
-
-          if(fun_name == (CONTRACTS_PREFIX "free"))
+          else if(fun_name == (CONTRACTS_PREFIX "free"))
             to_symbol_expr(ins->call_function()).set_identifier("free");
         }
       }