diff --git a/Data/SBV/BitVectors/STree.hs b/Data/SBV/BitVectors/STree.hs
--- a/Data/SBV/BitVectors/STree.hs
+++ b/Data/SBV/BitVectors/STree.hs
@@ -27,7 +27,7 @@
 -- elements of type i. Note that these are full-trees, and their
 -- their shapes remain constant. There is no API provided that
 -- can change the shape of the tree. These structures are useful
--- when dealing -- with data-structures that are indexed with symbolic
+-- when dealing with data-structures that are indexed with symbolic
 -- values where access time is important. 'STree' structures provide
 -- logarithmic time reads and writes.
 type STree i e = STreeInternal (SBV i) (SBV e)
diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs
--- a/Data/SBV/Compilers/C.hs
+++ b/Data/SBV/Compilers/C.hs
@@ -182,8 +182,11 @@
 genMake fn dn =
      text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!"
   $$ text ""
+  $$ text "# include any user-defined .mk file in the current directory."
+  $$ text "-include *.mk"
+  $$ text ""
   $$ text "CC=gcc"
-  $$ text "CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer"
+  $$ text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer"
   $$ text ""
   $$ text "all:" <+> nmd
   $$ text ""
@@ -515,8 +518,11 @@
 genLibMake libName fs =
      text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!"
   $$ text ""
+  $$ text "# include any user-defined .mk file in the current directory."
+  $$ text "-include *.mk"
+  $$ text ""
   $$ text "CC=gcc"
-  $$ text "CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer"
+  $$ text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer"
   $$ text "AR=ar"
   $$ text "ARFLAGS=cr"
   $$ text ""
diff --git a/Data/SBV/Examples/CodeGeneration/AddSub.hs b/Data/SBV/Examples/CodeGeneration/AddSub.hs
--- a/Data/SBV/Examples/CodeGeneration/AddSub.hs
+++ b/Data/SBV/Examples/CodeGeneration/AddSub.hs
@@ -25,8 +25,11 @@
 --
 -- > # Makefile for addSub. Automatically generated by SBV. Do not edit!
 -- > 
+-- > # include any user-defined .mk file in the current directory.
+-- > -include *.mk
+-- > 
 -- > CC=gcc
--- > CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+-- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 -- > 
 -- > all: addSub_driver
 -- > 
diff --git a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
--- a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
+++ b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
@@ -192,8 +192,11 @@
 --
 -- > # Makefile for popCount. Automatically generated by SBV. Do not edit!
 -- > 
+-- > # include any user-defined .mk file in the current directory.
+-- > -include *.mk
+-- > 
 -- > CC=gcc
--- > CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+-- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 -- > 
 -- > all: popCount_driver
 -- > 
diff --git a/README b/README
--- a/README
+++ b/README
@@ -115,8 +115,5 @@
 
 Thanks
 ======
-[Galois, Inc.](http://www.galois.com) has contributed to the development of SBV,
-by providing time and computing machinery.
-
 The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:
 Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
diff --git a/SBVUnitTest/GoldFiles/addSub.gold b/SBVUnitTest/GoldFiles/addSub.gold
--- a/SBVUnitTest/GoldFiles/addSub.gold
+++ b/SBVUnitTest/GoldFiles/addSub.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for addSub. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: addSub_driver
 
diff --git a/SBVUnitTest/GoldFiles/aes128Dec.gold b/SBVUnitTest/GoldFiles/aes128Dec.gold
--- a/SBVUnitTest/GoldFiles/aes128Dec.gold
+++ b/SBVUnitTest/GoldFiles/aes128Dec.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for aes128Dec. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: aes128Dec_driver
 
diff --git a/SBVUnitTest/GoldFiles/aes128Enc.gold b/SBVUnitTest/GoldFiles/aes128Enc.gold
--- a/SBVUnitTest/GoldFiles/aes128Enc.gold
+++ b/SBVUnitTest/GoldFiles/aes128Enc.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for aes128Enc. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: aes128Enc_driver
 
diff --git a/SBVUnitTest/GoldFiles/aes128Lib.gold b/SBVUnitTest/GoldFiles/aes128Lib.gold
--- a/SBVUnitTest/GoldFiles/aes128Lib.gold
+++ b/SBVUnitTest/GoldFiles/aes128Lib.gold
@@ -3733,8 +3733,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for aes128Lib. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 AR=ar
 ARFLAGS=cr
 
diff --git a/SBVUnitTest/GoldFiles/codeGen1.gold b/SBVUnitTest/GoldFiles/codeGen1.gold
--- a/SBVUnitTest/GoldFiles/codeGen1.gold
+++ b/SBVUnitTest/GoldFiles/codeGen1.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for foo. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: foo_driver
 
diff --git a/SBVUnitTest/GoldFiles/fib1.gold b/SBVUnitTest/GoldFiles/fib1.gold
--- a/SBVUnitTest/GoldFiles/fib1.gold
+++ b/SBVUnitTest/GoldFiles/fib1.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for fib1. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: fib1_driver
 
diff --git a/SBVUnitTest/GoldFiles/fib2.gold b/SBVUnitTest/GoldFiles/fib2.gold
--- a/SBVUnitTest/GoldFiles/fib2.gold
+++ b/SBVUnitTest/GoldFiles/fib2.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for fib2. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: fib2_driver
 
diff --git a/SBVUnitTest/GoldFiles/gcd.gold b/SBVUnitTest/GoldFiles/gcd.gold
--- a/SBVUnitTest/GoldFiles/gcd.gold
+++ b/SBVUnitTest/GoldFiles/gcd.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for sgcd. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: sgcd_driver
 
diff --git a/SBVUnitTest/GoldFiles/legato_c.gold b/SBVUnitTest/GoldFiles/legato_c.gold
--- a/SBVUnitTest/GoldFiles/legato_c.gold
+++ b/SBVUnitTest/GoldFiles/legato_c.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for legatoMult. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: legatoMult_driver
 
diff --git a/SBVUnitTest/GoldFiles/popCount1.gold b/SBVUnitTest/GoldFiles/popCount1.gold
--- a/SBVUnitTest/GoldFiles/popCount1.gold
+++ b/SBVUnitTest/GoldFiles/popCount1.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for popCount. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: popCount_driver
 
diff --git a/SBVUnitTest/GoldFiles/popCount2.gold b/SBVUnitTest/GoldFiles/popCount2.gold
--- a/SBVUnitTest/GoldFiles/popCount2.gold
+++ b/SBVUnitTest/GoldFiles/popCount2.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for popCount. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: popCount_driver
 
diff --git a/SBVUnitTest/GoldFiles/selChecked.gold b/SBVUnitTest/GoldFiles/selChecked.gold
--- a/SBVUnitTest/GoldFiles/selChecked.gold
+++ b/SBVUnitTest/GoldFiles/selChecked.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for selChecked. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: selChecked_driver
 
diff --git a/SBVUnitTest/GoldFiles/selUnchecked.gold b/SBVUnitTest/GoldFiles/selUnchecked.gold
--- a/SBVUnitTest/GoldFiles/selUnchecked.gold
+++ b/SBVUnitTest/GoldFiles/selUnchecked.gold
@@ -1,8 +1,11 @@
 == BEGIN: "Makefile" ================
 # Makefile for selUnChecked. Automatically generated by SBV. Do not edit!
 
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
 CC=gcc
-CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
 
 all: selUnChecked_driver
 
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       0.9.20
+Version:       0.9.21
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
 Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation.
 Description:   Express properties about bit-precise Haskell programs and automatically prove
@@ -51,10 +51,9 @@
                SBV is hosted at GitHub: <http://github.com/LeventErkok/sbv>. Comments,
                bug reports, and patches are always welcome.
                .
-               Galois, Inc. (<http://www.galois.com>) has contributed to the development of SBV,
-               by providing time and computing machinery. The following people reported bugs,
-               provided comments/feedback, or contributed to the development of SBV in various ways:
-               Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, and Josef Svenningsson.
+               The following people reported bugs, provided comments/feedback, or contributed to the
+               development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki,
+               Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.
 
 Copyright:     Levent Erkok, 2010-2011
 License:       BSD3