diff --git a/.gitignore b/.gitignore
index 7ba5ba011b4..082790b7126 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 *.obj
 *.a
 *.lib
+.release_info
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_library.inc
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 37f8b65eb00..c9f646f63ee 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -53,6 +53,14 @@ CLEANFILES = cbmc$(EXEEXT)
 
 all: cbmc$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_TAG_VERSION='"""$(CBMC_VERSION)"""' \
+       /DCBMC_VERSION='"""($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_TAG_VERSION="\"$(CBMC_VERSION)\"" \
+       -DCBMC_VERSION="\"($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../bv_refinement/Makefile),)
   OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 047e589accc..4414db851bf 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -55,7 +55,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "cbmc_solvers.h"
 #include "cbmc_parse_options.h"
 #include "bmc.h"
-#include "version.h"
 #include "xml_interface.h"
 
 /*******************************************************************\
@@ -1045,13 +1044,14 @@ void cbmc_parse_optionst::help()
 {
   std::cout <<
     "\n"
-    "* *   CBMC " CBMC_VERSION " - Copyright (C) 2001-2016 ";
+    "* *   CBMC " CBMC_TAG_VERSION " - Copyright (C) 2001-2016 ";
 
   std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
 
   std::cout << "   * *\n";
 
   std::cout <<
+    "* *                  " CBMC_VERSION "                * * \n"
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
     "* *                 kroening@kroening.com                   * *\n"
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index ccd660dc586..493df864d75 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bv_cbmc.h"
 #include "cbmc_dimacs.h"
 #include "counterexample_beautification.h"
-#include "version.h"
 
 /*******************************************************************\
 
diff --git a/src/cbmc/version.h b/src/cbmc/version.h
deleted file mode 100644
index 017ded44272..00000000000
--- a/src/cbmc/version.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef CPROVER_CBMC_VERSION_H
-#define CPROVER_CBMC_VERSION_H
-
-#define CBMC_VERSION "5.7"
-
-#endif // CPROVER_CBMC_VERSION_H
diff --git a/src/clobber/Makefile b/src/clobber/Makefile
index f3a4c8aed20..b0477115c8e 100644
--- a/src/clobber/Makefile
+++ b/src/clobber/Makefile
@@ -30,6 +30,12 @@ CLEANFILES = clobber$(EXEEXT)
 
 all: clobber$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../bv_refinement/Makefile),)
   OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 803ab9db5b1..e9067f594b3 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -32,8 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
-
 #include "clobber_parse_options.h"
 // #include "clobber_instrumenter.h"
 
diff --git a/src/common b/src/common
index 20c4fadbb44..d3022e8734a 100644
--- a/src/common
+++ b/src/common
@@ -1,3 +1,6 @@
+# get version from git
+GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
+
 # Build platform
 # (use one of AUTO, Unix, OSX, OSX_Universal, MSVC, Cygwin, MinGW)
 
@@ -182,12 +185,24 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 %.obj:%.c
 	$(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@
 
+# make >= 4.0 has a `file` function that may be faster than `shell cat`
+# for now, portability wins
+KNOWN_RELEASE_INFO = $(shell cat .release_info 2>/dev/null)
+ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
+$(filter %_parse_options$(OBJEXT), $(OBJ)): .release_info
+
+.release_info:
+	echo $(GIT_INFO) > $@
+
+.PHONY: .release_info
+endif
+
 clean:
 	$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
 		$(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \
 		$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
 		$(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \
-		$(CLEANFILES)
+		$(CLEANFILES) .release_info
 
 .PHONY: first_target clean all
 .PHONY: sources generated_files
@@ -207,4 +222,3 @@ D_FILES1 = $(SRC:.c=.d)
 D_FILES = $(D_FILES1:.cpp=.d)
 
 -include $(D_FILES)
-
diff --git a/src/config.inc b/src/config.inc
index e1c1266f683..7fede6e723d 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -28,3 +28,6 @@ MINISAT2 = ../../minisat-2.2.1
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
+
+# Detailed version information
+CBMC_VERSION = 5.7
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index 9eb45165f9c..b9e0a664330 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -30,6 +30,12 @@ CLEANFILES = goto-analyzer$(EXEEXT)
 
 all: goto-analyzer$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 5f889ff99d7..1d3c469fc20 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -42,8 +42,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string2int.h>
 #include <util/unicode.h>
 
-#include <cbmc/version.h>
-
 #include "goto_analyzer_parse_options.h"
 #include "taint_analysis.h"
 #include "unreachable_instructions.h"
diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
index 51ac3f0f9cb..50b25964c56 100644
--- a/src/goto-cc/Makefile
+++ b/src/goto-cc/Makefile
@@ -43,6 +43,12 @@ all: goto-cl$(EXEEXT)
 endif
 all: goto-cc$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
 endif
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
index bb87b6c6abb..308b549c581 100644
--- a/src/goto-cc/as_mode.cpp
+++ b/src/goto-cc/as_mode.cpp
@@ -24,8 +24,6 @@ Author: Michael Tautschnig
 #include <util/get_base_name.h>
 #include <util/cout_message.h>
 
-#include <cbmc/version.h>
-
 #include "compile.h"
 
 #include "as_mode.h"
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 04d50e76f82..7954313aec9 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -35,8 +35,6 @@ Date: June 2006
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
-
 #include "compile.h"
 
 #define DOTGRAPHSETTINGS  "color=black;" \
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 19444ef1fc5..4a10743be5a 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -26,8 +26,6 @@ Author: CM Wintersteiger, 2006
 #include <util/get_base_name.h>
 #include <util/run.h>
 
-#include <cbmc/version.h>
-
 #include "compile.h"
 #include "gcc_mode.h"
 
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index a0e363ad112..84957709d8d 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -17,7 +17,6 @@ Author: CM Wintersteiger, 2006
 #include <sysexits.h>
 #endif
 
-#include <cbmc/version.h>
 
 #include "goto_cc_mode.h"
 
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index 25dc0e039e2..006d3f8ebbd 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -22,8 +22,6 @@ Author: CM Wintersteiger, 2006
 #include <util/config.h>
 #include <util/get_base_name.h>
 
-#include <cbmc/version.h>
-
 #include "ms_cl_mode.h"
 #include "compile.h"
 
diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile
index b11cb008b3a..24d6795c94e 100644
--- a/src/goto-diff/Makefile
+++ b/src/goto-diff/Makefile
@@ -33,6 +33,12 @@ CLEANFILES = goto-diff$(EXEEXT)
 
 all: goto-diff$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index c66bd9817a6..e885953a3e4 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -36,8 +36,6 @@ Author: Peter Schrammel
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
-
 #include "goto_diff_parse_options.h"
 #include "goto_diff.h"
 #include "syntactic_diff.h"
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 4b74d173ff7..49478f61ddf 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -89,6 +89,12 @@ include ../common
 
 all: goto-instrument$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 66421b2e1e1..9760158a8b6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -55,8 +55,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/constant_propagator.h>
 #include <analyses/is_threaded.h>
 
-#include <cbmc/version.h>
-
 #include "goto_instrument_parse_options.h"
 #include "document_properties.h"
 #include "uninitialized.h"
diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile
index e13309deaae..ab9c6114473 100644
--- a/src/memory-models/Makefile
+++ b/src/memory-models/Makefile
@@ -21,6 +21,12 @@ CLEANFILES = memory_models$(LIBEXT) \
 
 all: mmcc$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ###############################################################################
 
 mm_y.tab.cpp: parser.y
diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp
index 859393f9726..71c0337280e 100644
--- a/src/memory-models/mmcc_parse_options.cpp
+++ b/src/memory-models/mmcc_parse_options.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/cout_message.h>
 
-#include <cbmc/version.h>
-
 #include "mm_parser.h"
 #include "mm2cpp.h"
 #include "mmcc_parse_options.h"
diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile
index be41fa923cc..950b7850a46 100644
--- a/src/musketeer/Makefile
+++ b/src/musketeer/Makefile
@@ -46,6 +46,12 @@ include ../common
 
 all: musketeer$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DMUSKETEER_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DMUSKETEER_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
   CP_CXXFLAGS += -DHAVE_GLPK
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index ae40a2f2318..6d26707b36c 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -38,7 +38,6 @@ Module: Main Module
 #include <goto-instrument/wmm/weak_memory.h>
 
 #include "propagate_const_function_pointers.h"
-#include "version.h"
 #include "musketeer_parse_options.h"
 #include "fencer.h"
 #include "fence_shared.h"
diff --git a/src/musketeer/version.h b/src/musketeer/version.h
deleted file mode 100644
index fde0c82ecea..00000000000
--- a/src/musketeer/version.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef CPROVER_MUSKETEER_VERSION_H
-#define CPROVER_MUSKETEER_VERSION_H
-
-#define MUSKETEER_VERSION "0.37"
-
-#endif // CPROVER_MUSKETEER_VERSION_H
diff --git a/src/symex/Makefile b/src/symex/Makefile
index 672b2e07fc2..455626a106c 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -34,6 +34,12 @@ CLEANFILES = symex$(EXEEXT)
 
 all: symex$(EXEEXT)
 
+ifeq ($(BUILD_ENV_),MSVC)
+  CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
+else
+  CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
+endif
+
 ifneq ($(wildcard ../bv_refinement/Makefile),)
   OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 8001a5b8155..1906d7615ce 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -43,8 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
-
 #include <path-symex/locs.h>
 
 #include "path_search.h"