diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index f8225e0d4..a9dddd6f2 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -193,16 +193,16 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g) {
+    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names) {
         Z3_TRY;
-        LOG_Z3_goal_to_dimacs_string(c, g);
+        LOG_Z3_goal_to_dimacs_string(c, g, include_names);
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         if (!to_goal_ref(g)->is_cnf()) { 
             SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
             RETURN_Z3(nullptr);
         }
-        to_goal_ref(g)->display_dimacs(buffer, true);
+        to_goal_ref(g)->display_dimacs(buffer, include_names);
         // Hack for removing the trailing '\n'
         std::string result = buffer.str();
         SASSERT(result.size() > 0);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1e297cf05..425e2e314 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2630,7 +2630,7 @@ namespace z3 {
                 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
             }
         }
-        std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); }
+        std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
         friend std::ostream & operator<<(std::ostream & out, goal const & g);
     };
     inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 883b91f35..05edb36b1 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -225,9 +225,9 @@ namespace Microsoft.Z3
         /// Goal to DIMACS formatted string conversion.
         /// </summary>
         /// <returns>A string representation of the Goal.</returns>
-        public string ToDimacs()
+        public string ToDimacs(bool include_names = true)
         {
-            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject);
+            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, include_names);
         }
 
         /// <summary>
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index b5d33ff6c..2e2de4e23 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -5413,9 +5413,9 @@ class Goal(Z3PPObject):
         """Return a textual representation of the s-expression representing the goal."""
         return Z3_goal_to_string(self.ctx.ref(), self.goal)
 
-    def dimacs(self):
+    def dimacs(self, include_names = True):
         """Return a textual representation of the goal in DIMACS format."""
-        return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal)
+        return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal, include_names)
 
     def translate(self, target):
         """Copy goal `self` to context `target`.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index fbe7eb40f..4311a0bdb 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5840,9 +5840,9 @@ extern "C" {
        preserve satisfiability, it should apply bit-blasting tactics.
        Quantifiers and theory atoms will not be encoded.
 
-       def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL)))
+       def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g);
+    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names);
 
     /*@}*/