diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 41d176e8dd9..5865f49f154 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
+          dynamic_cast<bv_cbmct &>(prop_conv), equation);
 
       error_trace();
       output_graphml(resultt::UNSAFE);
diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp
index 9522107d922..89cb4c119bb 100644
--- a/src/cbmc/counterexample_beautification.cpp
+++ b/src/cbmc/counterexample_beautification.cpp
@@ -80,8 +80,7 @@ counterexample_beautificationt::get_failed_property(
 
 void counterexample_beautificationt::operator()(
   bv_cbmct &bv_cbmc,
-  const symex_target_equationt &equation,
-  const namespacet &ns)
+  const symex_target_equationt &equation)
 {
   // find failed property
 
diff --git a/src/cbmc/counterexample_beautification.h b/src/cbmc/counterexample_beautification.h
index 10bb96f4597..d05f004d471 100644
--- a/src/cbmc/counterexample_beautification.h
+++ b/src/cbmc/counterexample_beautification.h
@@ -29,8 +29,7 @@ class counterexample_beautificationt
 
   void operator()(
     bv_cbmct &bv_cbmc,
-    const symex_target_equationt &equation,
-    const namespacet &ns);
+    const symex_target_equationt &equation);
 
 protected:
   void get_minimization_list(
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index 1c8a6741f65..104c049394b 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -281,7 +281,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);
+          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation);
 
       bmc.error_trace();
     }