diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Examples/Uninterpreted/Function.hs
@@ -0,0 +1,42 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Examples.Uninterpreted.Function
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Demonstrates function counter-examples
+-----------------------------------------------------------------------------
+
+module Data.SBV.Examples.Uninterpreted.Function where
+
+import Data.SBV
+
+-- | An uninterpreted function
+f :: SWord8 -> SWord8 -> SWord16
+f = uninterpret "f"
+
+-- | Asserts that @f x z == f (y+2) z@ whenever @x == y+2@. Naturally correct.
+thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
+thmGood x y z = x .== y+2 ==> f x z .== f (y + 2) z
+
+-- | Asserts that @f@ is commutative; which is not necessarily true!
+-- Indeed, the SMT solver (Yices in this case) returns a counter-example
+-- function that is not commutative. We have:
+--
+-- @
+-- ghci> prove thmBad
+-- Falsifiable. Counter-example:
+--   s0 = 0 :: SWord8
+--   s1 = 128 :: SWord8
+--   -- uninterpreted: f
+--        f 128 0 = 32768
+--        f _ _ = 0
+-- @
+--
+-- Note how the counterexample function @f@ returned by Yices violates commutativity;
+-- thus providing evidence that the asserted theorem is not valid.
+thmBad :: SWord8 -> SWord8 -> SBool
+thmBad x y = f x y .== f y x
diff --git a/Data/SBV/TestSuite/Uninterpreted/Function.hs b/Data/SBV/TestSuite/Uninterpreted/Function.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/TestSuite/Uninterpreted/Function.hs
@@ -0,0 +1,24 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.TestSuite.Uninterpreted.Function
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Testsuite for Data.SBV.Examples.Uninterpreted.Function
+-----------------------------------------------------------------------------
+
+module Data.SBV.TestSuite.Uninterpreted.Function where
+
+import Data.SBV
+import Data.SBV.Internals
+import Data.SBV.Examples.Uninterpreted.Function
+
+-- Test suite
+testSuite :: SBVTestSuite
+testSuite = mkTestSuite $ \_ -> test [
+   "aufunc-0" ~: assert       =<< isTheorem thmGood
+ , "aufunc-1" ~: assert . not =<< isTheorem thmBad
+ ]
diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs
--- a/SBVUnitTest/SBVUnitTest.hs
+++ b/SBVUnitTest/SBVUnitTest.hs
@@ -49,7 +49,8 @@
 import qualified Data.SBV.TestSuite.Puzzles.Temperature           as T22(testSuite)
 import qualified Data.SBV.TestSuite.Puzzles.U2Bridge              as T23(testSuite)
 import qualified Data.SBV.TestSuite.Uninterpreted.AUF             as T24(testSuite)
-import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted   as T25(testSuite)
+import qualified Data.SBV.TestSuite.Uninterpreted.Function        as T25(testSuite)
+import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted   as T26(testSuite)
 
 testCollection :: [SBVTestSuite]
 testCollection = [
@@ -59,7 +60,7 @@
      , T13.testSuite, T14.testSuite, T15.testSuite, T16.testSuite
      , T17.testSuite, T18.testSuite, T19.testSuite, T20.testSuite
      , T21.testSuite, T22.testSuite, T23.testSuite, T24.testSuite
-     , T25.testSuite
+     , T25.testSuite, T26.testSuite
      ]
 -- No user serviceable parts below..
 
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       0.9.5
+Version:       0.9.6
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
 Synopsis:      Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.
 Description:   Adds support for symbolic bit vectors, allowing formal models of bit-precise
@@ -49,6 +49,7 @@
                   , Data.SBV.Examples.Puzzles.Sudoku
                   , Data.SBV.Examples.Puzzles.U2Bridge
                   , Data.SBV.Examples.Uninterpreted.AUF
+                  , Data.SBV.Examples.Uninterpreted.Function
   Other-modules   : Data.SBV.BitVectors.Data
                   , Data.SBV.BitVectors.Bit
                   , Data.SBV.BitVectors.Model
@@ -104,6 +105,7 @@
                   , Data.SBV.TestSuite.Puzzles.Temperature
                   , Data.SBV.TestSuite.Uninterpreted.AUF
                   , Data.SBV.TestSuite.Uninterpreted.Uninterpreted
+                  , Data.SBV.TestSuite.Uninterpreted.Function
 
 Executable SBVUnitTests
   main-is         : SBVUnitTest/SBVUnitTest.hs