diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs
index 33f8de06d..9ee6ef51f 100644
--- a/Data/SBV/Control/Utils.hs
+++ b/Data/SBV/Control/Utils.hs
@@ -929,7 +929,7 @@ recoverKindedValue k e = case k of
                                        | EReal i     <- e      -> Just $ CV KReal (CAlgReal i)
                                        | True                  -> interpretInterval e
 
-                           KUserSort{} | ECon s <- e           -> Just $ CV k $ CUserSort (getUIIndex k s, s)
+                           KUserSort{} | ECon s <- e           -> Just $ CV k $ CUserSort (getUIIndex k s, trim s)
                                        | True                  -> Nothing
 
                            KFloat      | ENum (i, _) <- e      -> Just $ mkConstCV k i
@@ -965,6 +965,11 @@ recoverKindedValue k e = case k of
 
         stringLike xs = length xs >= 2 && "\"" `isPrefixOf` xs && "\"" `isSuffixOf` xs
 
+        -- z3 prints uninterpreted values like this: T!val!4. Turn that into T_4
+        trim "" = ""
+        trim ('!':'v':'a':'l':'!':rest) = '_' : trim rest
+        trim (c:cs) = c : trim cs
+
         -- Make sure strings are really strings
         interpretString xs
           | not (stringLike xs)
diff --git a/Documentation/SBV/Examples/KnuckleDragger/Basics.hs b/Documentation/SBV/Examples/KnuckleDragger/Basics.hs
index eb3ea5257..a1783376c 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Basics.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Basics.hs
@@ -116,14 +116,14 @@ existsDisjunction = runKD $ do
 -- *** Failed to prove forallConjunctionNot.
 -- Falsifiable. Counter-example:
 --   p :: T -> Bool
---   p T!val!2 = True
---   p T!val!0 = True
---   p _       = False
+--   p T_2 = True
+--   p T_0 = True
+--   p _   = False
 -- <BLANKLINE>
 --   q :: T -> Bool
---   q T!val!2 = False
---   q T!val!0 = False
---   q _       = True
+--   q T_2 = False
+--   q T_0 = False
+--   q _   = True
 --
 -- Note how @p@ assigns two selected values to @True@ and everything else to @False@, while @q@ does the exact opposite.
 -- So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds
@@ -153,12 +153,12 @@ forallDisjunctionNot = runKD $ do
 -- *** Failed to prove existsConjunctionNot.
 -- Falsifiable. Counter-example:
 --   p :: T -> Bool
---   p T!val!1 = False
---   p _       = True
+--   p T_1 = False
+--   p _   = True
 -- <BLANKLINE>
 --   q :: T -> Bool
---   q T!val!1 = True
---   q _       = False
+--   q T_1 = True
+--   q _   = False
 --
 -- In this case, we again have a predicate That disagree at every point, providing a counter-example.
 existsConjunctionNot :: IO ()
diff --git a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
index 828bd6b14..c4b494487 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs
@@ -66,7 +66,7 @@ revLen = runKD $ do
 -- Lemma: badRevLen
 -- *** Failed to prove badRevLen.
 -- Falsifiable. Counter-example:
---   xs = [Elt!val!1,Elt!val!2,Elt!val!1] :: [Elt]
+--   xs = [Elt_1,Elt_2,Elt_1] :: [Elt]
 badRevLen :: IO ()
 badRevLen = runKD $ do
    let p :: SList Elt -> SBool
diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
index 4ce071733..c426fbbed 100644
--- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
@@ -132,20 +132,20 @@ We have:
 >>> prove $ (qe (\(Forall x) -> p x) .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .|| q x)
 Falsifiable. Counter-example:
   P :: U -> Bool
-  P U!val!2 = True
-  P U!val!0 = True
-  P _       = False
+  P U_2 = True
+  P U_0 = True
+  P _   = False
 <BLANKLINE>
   Q :: U -> Bool
-  Q U!val!2 = False
-  Q U!val!0 = False
-  Q _       = True
+  Q U_2 = False
+  Q U_0 = False
+  Q _   = True
 
 The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call
-the first element @U!val!2@, and the second element @U!val!0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct
+the first element @U_2@, and the second element @U_0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct
 objects that belong to the domain \(U\) with no other meaning.)
 
-Arrange so that \(P\) is true on @U!val!2@ and @U!val!0@, but false for everything else.
+Arrange so that \(P\) is true on @U_2@ and @U_0@, but false for everything else.
 Also arrange so that \(Q\) is false on these two elements, but true for everything else.
 
 With this
diff --git a/Documentation/SBV/Examples/Uninterpreted/Sort.hs b/Documentation/SBV/Examples/Uninterpreted/Sort.hs
index 5bb3fade3..5ec20bb4e 100644
--- a/Documentation/SBV/Examples/Uninterpreted/Sort.hs
+++ b/Documentation/SBV/Examples/Uninterpreted/Sort.hs
@@ -39,10 +39,10 @@ f = uninterpret "f"
 --
 -- >>> t1
 -- Satisfiable. Model:
---   x = Q!val!0 :: Q
+--   x = Q_0 :: Q
 -- <BLANKLINE>
 --   f :: Q -> Q
---   f _ = Q!val!1
+--   f _ = Q_1
 t1 :: IO SatResult
 t1 = sat $ do x <- free "x"
               return $ f x ./= x
diff --git a/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs
index 87187a655..132a19a92 100644
--- a/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs
+++ b/Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs
@@ -54,35 +54,35 @@ classify = uninterpret "classify"
 --
 -- >>> allSat genLs
 -- Solution #1:
---   l  = L!val!2 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_2 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Solution #2:
---   l  = L!val!1 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_1 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Solution #3:
---   l  = L!val!0 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_0 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Found 3 different solutions.
 genLs :: Predicate
 genLs = do [l, l0, l1, l2] <- symbolics ["l", "l0", "l1", "l2"]
diff --git a/SBVTestSuite/GoldFiles/allSat1.gold b/SBVTestSuite/GoldFiles/allSat1.gold
index 41f9d40cb..292c1f0f3 100644
--- a/SBVTestSuite/GoldFiles/allSat1.gold
+++ b/SBVTestSuite/GoldFiles/allSat1.gold
@@ -1,4 +1,4 @@
 Solution #1:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-This is the only solution.
\ No newline at end of file
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+This is the only solution.
diff --git a/SBVTestSuite/GoldFiles/allSat2.gold b/SBVTestSuite/GoldFiles/allSat2.gold
index c39c5c363..d5568a383 100644
--- a/SBVTestSuite/GoldFiles/allSat2.gold
+++ b/SBVTestSuite/GoldFiles/allSat2.gold
@@ -1,9 +1,9 @@
 Solution #1:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-  z = Q!val!1 :: Q
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+  z = Q_1 :: Q
 Solution #2:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-  z = Q!val!0 :: Q
-Found 2 different solutions.
\ No newline at end of file
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+  z = Q_0 :: Q
+Found 2 different solutions.
diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4.gold b/SBVTestSuite/GoldFiles/uninterpreted-4.gold
index 05c2056c0..745f5aec1 100644
--- a/SBVTestSuite/GoldFiles/uninterpreted-4.gold
+++ b/SBVTestSuite/GoldFiles/uninterpreted-4.gold
@@ -36,6 +36,6 @@
 *** Exit code: ExitSuccess
 
  FINAL:Satisfiable. Model:
-  c = Q!val!0 :: Q
-  d = Q!val!1 :: Q
+  c = Q_0 :: Q
+  d = Q_1 :: Q
 DONE!
diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4a.gold b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold
index 6ef097e2a..b59895528 100644
--- a/SBVTestSuite/GoldFiles/uninterpreted-4a.gold
+++ b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold
@@ -46,7 +46,7 @@ Looking for solution 1
 *** Exit code: ExitSuccess
 
  FINAL:Solution #1:
-  c = Q!val!0 :: Q
-  d = Q!val!1 :: Q
+  c = Q_0 :: Q
+  d = Q_1 :: Q
 This is the only solution.
 DONE!
diff --git a/sbv.cabal b/sbv.cabal
index 8fd44d5f8..47531be16 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -159,6 +159,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.CaseSplit
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
+                  , Documentation.SBV.Examples.KnuckleDragger.InsertionSort
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen
                   , Documentation.SBV.Examples.KnuckleDragger.RevLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational