diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,32 @@
+2018-08-29  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* cpsa.cabal (Version): Tagged as 3.6.1
+
+2018-08-22  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Strand.hs (doRewrites): Added a limit on the number of
+	rules that can be applied after solving an authentication test.
+
+2018-08-20  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Strand.hs (cleansPreskel): Cleansed facts from a
+	skeleton purged of a strand.  This changes fixes a nasty display
+	bug that occurred when a variable in a fact did not occur in any
+	strand.
+
+2018-08-06  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/CPSA/Lib/Loader.hs (loadConclusion):  Removed mode flag as
+	this routine should always be using mode RoleSpec.  This resolves
+	a bug in which CPSA could not load a Shape Analysis Sentence as
+	rule because equality was before the protocol specific formulas.
+
+	* src/CPSA/Lib/Strand.hs (newPreskel):  Changed newPreskel so that
+	it removed duplicates in the leadsto field when creating a new
+	preskeleton.  This resolved a bug in which CPSA produced to shapes
+	that appeared to be isomorphic, but instead, one shape had
+	duplicates in its leadsto field.
+
 2018-06-25  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* cpsa.cabal (Version): Tagged as 3.6.0
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,10 @@
 CPSA NEWS
 
+  August, 2018:
+
+* Release 3.6.1 is a bug fix release.  It includes updates to the CPSA
+  manual.  There are no user visible changes.
+
   June, 2018:
 
 * Release 3.6.0 adds rules and facts.  Rules are associated with
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -1,5 +1,5 @@
 Name:			cpsa
-Version:		3.6.0
+Version:		3.6.1
 Maintainer:		mliskov@mitre.org
 Cabal-Version:		>= 1.6
 License:		BSD3
diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf
Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ
diff --git a/src/CPSA/Lib/Loader.hs b/src/CPSA/Lib/Loader.hs
--- a/src/CPSA/Lib/Loader.hs
+++ b/src/CPSA/Lib/Loader.hs
@@ -922,7 +922,7 @@
 loadImplication md _ prot g vars (L pos [S _ "implies", a, c]) =
   do
     antec <- loadCheckedConj md pos prot vars vars a
-    (g, vc) <- loadConclusion md pos prot g vars c
+    (g, vc) <- loadConclusion pos prot g vars c
     let (evars, concl) = unzip vc
     let goal =
           Goal { uvars = vars,
@@ -935,35 +935,35 @@
 -- The conclusion must be a disjunction.  Each disjunct may introduce
 -- existentially quantified variables.
 
-loadConclusion :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->
+loadConclusion :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
                   g -> [t] -> SExpr Pos -> m (g, [([t], Conj t)])
-loadConclusion _ _ _ g _ (L _ [S _ "false"]) = return (g, [])
-loadConclusion md _ prot g vars (L pos (S _ "or" : xs)) =
-  loadDisjuncts md pos prot g vars xs []
-loadConclusion md pos prot g vars x =
+loadConclusion _ _ g _ (L _ [S _ "false"]) = return (g, [])
+loadConclusion _ prot g vars (L pos (S _ "or" : xs)) =
+  loadDisjuncts pos prot g vars xs []
+loadConclusion pos prot g vars x =
   do
-    (g, a) <- loadExistential md pos prot g vars x
+    (g, a) <- loadExistential pos prot g vars x
     return (g, [a])
 
-loadDisjuncts :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->
+loadDisjuncts :: (Algebra t p g s e c, Monad m) => Pos ->
                  Prot t g -> g -> [t] -> [SExpr Pos] ->
                  [([t], Conj t)] -> m (g, [([t], Conj t)])
-loadDisjuncts _ _ _ g _ [] rest = return (g, reverse rest)
-loadDisjuncts md pos prot g vars (x : xs) rest =
+loadDisjuncts _ _ g _ [] rest = return (g, reverse rest)
+loadDisjuncts pos prot g vars (x : xs) rest =
   do
-    (g, a) <- loadExistential md pos prot g vars x
-    loadDisjuncts md pos prot g vars xs (a : rest)
+    (g, a) <- loadExistential pos prot g vars x
+    loadDisjuncts pos prot g vars xs (a : rest)
 
-loadExistential :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->
+loadExistential :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->
                    g -> [t] -> SExpr Pos -> m (g, ([t], Conj t))
-loadExistential md _ prot g vars (L pos [S _ "exists", L _ vs, x]) =
+loadExistential _ prot g vars (L pos [S _ "exists", L _ vs, x]) =
   do
     (g, evars) <- loadVars g vs
-    as <- loadCheckedConj md pos prot (evars ++ vars) evars x
+    as <- loadCheckedConj RoleSpec pos prot (evars ++ vars) evars x
     return (g, (evars, as))
-loadExistential md pos prot g vars x =
+loadExistential pos prot g vars x =
   do
-    as <- loadCheckedConj md pos prot vars [] x
+    as <- loadCheckedConj RoleSpec pos prot vars [] x
     return (g, ([], as))
 
 -- Load a conjunction and check the result as determined by the mode
@@ -1090,7 +1090,7 @@
           Nothing ->
             fail (shows pos ("parameter " ++ x ++ " not in role " ++ name))
 loadPrimary _ _ _ (L pos (S _ "p" : Q _ name : _)) =
-  fail (shows pos ("Malformed role specific formula for role " ++ name))
+  fail (shows pos ("Malformed protocol specific formula for role " ++ name))
 loadPrimary _ _ _ (L pos (S _ pred : _)) =
   fail (shows pos ("Malformed formula for predicate " ++ pred))
 loadPrimary pos _ _ _ = fail (shows pos "Bad formula")
diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs
--- a/src/CPSA/Lib/Reduction.hs
+++ b/src/CPSA/Lib/Reduction.hs
@@ -39,7 +39,7 @@
 
 -- Set when debugging an exception so that buffered results get out.
 useFlush :: Bool
-useFlush = True                -- False
+useFlush = False                -- True
 
 -- Parameter driven S-expression printer
 wrt :: Options -> Handle -> SExpr a -> IO ()
diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs
--- a/src/CPSA/Lib/Strand.hs
+++ b/src/CPSA/Lib/Strand.hs
@@ -517,6 +517,7 @@
 newPreskel gen shared insts orderings leadsto decls
            facts oper prob kpriority pov =
     let orderings' = L.nub orderings
+        leadsto' = L.nub leadsto
         g = graph trace height insts orderings'
         strands = gstrands g
         decls' = declsNub decls
@@ -528,7 +529,7 @@
                       insts = insts,
                       strands = strands,
                       orderings = orderings',
-                      leadsto = leadsto,
+                      leadsto = leadsto',
                       edges = edges,
                       decls = decls',
                       extraDecls = mkDecls [],
@@ -835,6 +836,7 @@
     checkOrigs g g' fenv perm &&
     checkOrigs g' g renv (invperm perm) &&
     checkFacts g g' fenv perm &&
+    checkFacts g' g fenv (invperm perm) &&
     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&
     containsMapped (permutePair perm) (gleadsto g') (gleadsto g)
 
@@ -844,6 +846,7 @@
     checkOrigs g g' fenv perm &&
     checkOrigs g' g renv perm &&
     checkFacts g g' fenv perm &&
+    checkFacts g' g fenv (invperm perm) &&
     containsMapped (permutePair perm) (gorderings g') (gorderings g) &&
     containsMapped (permutePair perm) (gleadsto g') (gleadsto g) &&
     all (\n -> perm !! (prob !! n) == prob' !! n) [0..((length prob)-1)]
@@ -1048,7 +1051,7 @@
               (updateProb perm (prob k))
               (updatePriority perm (kpriority k))
               (pov k)
-      k'' <- wellFormedPreskel $ k'
+      k'' <- wellFormedPreskel $ cleansPreskel k'
       return (k0, k'', permuteNode perm n, map (perm !!) phi, hsubst)
 
 -- Forward orderings from strand s
@@ -1063,6 +1066,22 @@
           | s1 == s = []        -- Dump edges to strand s
           | otherwise = [p]     -- Pass thru other edges
 
+-- Cleans facts in a skeleton
+cleansPreskel :: Algebra t p g s e c => Preskel t g s e ->  Preskel t g s e
+cleansPreskel k =
+  newPreskel
+  (gen k)
+  (shared k)
+  (insts k)
+  (orderings k)
+  (leadsto k)
+  (decls k)
+  (cleansFacts (kvars k) (kfacts k))
+  (operation k)
+  (prob k)
+  (kpriority k)
+  (pov k)
+
 matchTraces :: Algebra t p g s e c => Trace t ->
                Trace t -> (g, e) -> [(g, e)]
 matchTraces [] _ env = [env]    -- Pattern can be shorter
@@ -1531,6 +1550,8 @@
                Preskel t g s e -> [Sid] -> e -> Bool
 validateEnv k k' mapping env =
   validateDeclEnv k k' mapping env &&
+  all (flip elem (kfacts k'))
+  (map (instUpdateFact env (mapping !!)) (kfacts k)) &&
   all (flip elem (tc k')) (permuteOrderings mapping (orderings k))
 
 -- Given a realized skeleton k, generate candidates for minimization.
@@ -2551,20 +2572,30 @@
 -}
 
 {-- For debugging
-factVars :: Fact -> [Term] -> [Term]
+factVars :: Algebra t p g s e c => Fact t -> [t] -> [t]
 factVars (Fact _ ts) vs =
   foldr f vs ts
   where
     f (FSid _) vs = vs
     f (FTerm t) vs = addVars vs t
 
-chkFVars :: Preskel -> Preskel
+chkFVars :: Algebra t p g s e c => Preskel t g s e -> Preskel t g s e
 chkFVars k =
   foldl f k (foldr factVars [] (kfacts k))
   where
     f k v
       | elem v (kvars k) = k
       | otherwise = error ("Bad var in fact " ++ show v)
+        -- ++ "\n\n" ++ show k)
+
+chkFVarsS :: Algebra t p g s e c => String -> Preskel t g s e -> Preskel t g s e
+chkFVarsS s k =
+  foldl f k (foldr factVars [] (kfacts k))
+  where
+    f k v
+      | elem v (kvars k) = k
+      | otherwise = error (s ++ ": Bad var in fact " ++ show v)
+        -- ++ "\n\n" ++ show k)
 --}
 
 {-
@@ -2613,6 +2644,12 @@
 -- eliminate error cases.
 geq :: Algebra t p g s e c => t -> t -> Sem t g s e
 geq t t' _ (g, e)
+  -- Ensure all variables in t and t' are in the domain of e.
+  -- This always happens for goals because they must be role specific
+  -- but it is not always true for rules.
+  | not (matched e t) || not (matched e t') =
+      error ("In a rule equality check, " ++
+             "cannot find a binding for some variable")
   | ti == ti' = [(g, e)]
   | otherwise = []
   where
@@ -2721,12 +2758,14 @@
   case (nodeLookup e n, nodeLookup e n') of
     (Just p, Just p')
       | inSkel k p && inSkel k p' &&
-        (strandPrec p p' || elem (p, p') (tc k)) -> [(g, e)]
+        (strandPrec p p' || elem (p, p') tc) -> [(g, e)]
     _ ->
       do
-        (p, p') <- tc k
+        (p, p') <- tc
         (g, e) <- nodeMatch n p (g, e)
         nodeMatch n' p' (g, e)
+  where
+    tc = map graphPair $ graphClose $ graphEdges $ strands k
 
 -- Length predicate
 -- r and h determine the predicate, which has arity one.
@@ -2843,7 +2882,7 @@
         if null vas then
           loop rs               -- Rule does not apply
         else
-          Just $ doRewrites prules k r vas
+          Just $ doRewrites 0 prules k r vas
 
 -- Returns the environments that show satifaction of the antecedent
 -- but fail to be extendable to show satifaction of one of the
@@ -2856,10 +2895,17 @@
     conclusion e = all (disjunct e) $ concl $ rlgoal r
     disjunct e a = null $ conjoin a k e
 
+ruleLimit :: Int
+ruleLimit = 500
+
 -- Repeatedly applies rules until no rule applies.
-doRewrites :: Algebra t p g s e c => [Rule t] -> Preskel t g s e ->
+doRewrites :: Algebra t p g s e c => Int -> [Rule t] -> Preskel t g s e ->
               Rule t -> [(g, e)] -> [Preskel t g s e]
-doRewrites rules k r vas =
+doRewrites lim _ _ _ _
+  | lim >= ruleLimit =
+    error ("Aborting after applying " ++ show ruleLimit ++
+           " rules and more are applicable")
+doRewrites lim rules k r vas =
   concatMap f (doRewrite k r vas)
   where
     f k = loop rules
@@ -2870,7 +2916,7 @@
             if null vas then
               loop rs           -- Rule does not apply
             else
-              doRewrites rules k r vas
+              doRewrites (lim + 1) rules k r vas
 
 -- Apply rewrite rule at all assignments
 doRewrite :: Algebra t p g s e c => Preskel t g s e ->
@@ -3049,7 +3095,7 @@
                    (prob k) (kpriority k) (pov k)
           return (k', (gen k, e))
     _ ->
-      error ("In rule " ++ name ++ ", precidence did not get a strand")
+      error ("In rule " ++ name ++ ", precedence did not get a strand")
   where
     tc = map graphPair $ graphClose $ graphEdges $ strands k
 
diff --git a/tst/aik.tst b/tst/aik.tst
--- a/tst/aik.tst
+++ b/tst/aik.tst
@@ -1,6 +1,6 @@
 (herald "Anonymous identity protocol from TCG")
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from aik.scm")
 
 (defprotocol aikprot basic
diff --git a/tst/axiom2.tst b/tst/axiom2.tst
--- a/tst/axiom2.tst
+++ b/tst/axiom2.tst
@@ -1,6 +1,6 @@
 (herald "Axiom 2 Protocol" (bound 20))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from axiom2.scm")
 (comment "Strand count bounded at 20")
 
diff --git a/tst/blanchet.tst b/tst/blanchet.tst
--- a/tst/blanchet.tst
+++ b/tst/blanchet.tst
@@ -1,7 +1,7 @@
 (herald "Blanchet's Simple Example Protocol"
   (comment "There is a flaw in this protocol by design"))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from blanchet.scm")
 
 (defprotocol blanchet basic
diff --git a/tst/bltk_test.tst b/tst/bltk_test.tst
--- a/tst/bltk_test.tst
+++ b/tst/bltk_test.tst
@@ -1,6 +1,6 @@
 (herald "bltk Test File" (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from bltk_test.scm")
 
 (defprotocol test diffie-hellman
diff --git a/tst/dh-ca.tst b/tst/dh-ca.tst
--- a/tst/dh-ca.tst
+++ b/tst/dh-ca.tst
@@ -1,6 +1,6 @@
 (herald dhca (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dh-ca.scm")
 
 (defprotocol dhca diffie-hellman
diff --git a/tst/dh_mim.tst b/tst/dh_mim.tst
--- a/tst/dh_mim.tst
+++ b/tst/dh_mim.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dh_mim.scm")
 
 (defprotocol dh_mim diffie-hellman
diff --git a/tst/dh_mim2.tst b/tst/dh_mim2.tst
--- a/tst/dh_mim2.tst
+++ b/tst/dh_mim2.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dh_mim2.scm")
 
 (defprotocol dh_mim diffie-hellman
diff --git a/tst/dh_sig.tst b/tst/dh_sig.tst
--- a/tst/dh_sig.tst
+++ b/tst/dh_sig.tst
@@ -1,6 +1,6 @@
 (herald "Signed DH exchange" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dh_sig.scm")
 
 (defprotocol dh_sig diffie-hellman
diff --git a/tst/dh_test.tst b/tst/dh_test.tst
--- a/tst/dh_test.tst
+++ b/tst/dh_test.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman protocol, man-in-the-middle attack"
   (algebra diffie-hellman) (bound 20))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dh_test.scm")
 (comment "Strand count bounded at 20")
 
diff --git a/tst/dhnsl_basic.tst b/tst/dhnsl_basic.tst
--- a/tst/dhnsl_basic.tst
+++ b/tst/dhnsl_basic.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dhnsl_basic.scm")
 
 (defprotocol dhnsl diffie-hellman
diff --git a/tst/dhnsl_use.tst b/tst/dhnsl_use.tst
--- a/tst/dhnsl_use.tst
+++ b/tst/dhnsl_use.tst
@@ -1,7 +1,7 @@
 (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from dhnsl_use.scm")
 
 (defprotocol dhnsl diffie-hellman
diff --git a/tst/enrich.tst b/tst/enrich.tst
--- a/tst/enrich.tst
+++ b/tst/enrich.tst
@@ -1,6 +1,6 @@
 (herald enrich)
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from enrich.scm")
 
 (defprotocol enrich basic
diff --git a/tst/envelope.tst b/tst/envelope.tst
--- a/tst/envelope.tst
+++ b/tst/envelope.tst
@@ -1,6 +1,6 @@
 (herald "Envelope Protocol" (bound 20))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from envelope.scm")
 (comment "Strand count bounded at 20")
 
diff --git a/tst/ffgg.tst b/tst/ffgg.tst
--- a/tst/ffgg.tst
+++ b/tst/ffgg.tst
@@ -1,7 +1,7 @@
 (herald "The ffgg Protocol"
   (comment "From A Necessarily Parallel Attack by Jon K. Millen"))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from ffgg.scm")
 
 (defprotocol ffgg basic
diff --git a/tst/fnof_or.tst b/tst/fnof_or.tst
--- a/tst/fnof_or.tst
+++ b/tst/fnof_or.tst
@@ -2,7 +2,7 @@
   (comment
     "Version using variables of sort mesg, with ltk function emulated."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from fnof_or.scm")
 
 (defprotocol or basic
diff --git a/tst/fnof_test.tst b/tst/fnof_test.tst
--- a/tst/fnof_test.tst
+++ b/tst/fnof_test.tst
@@ -1,7 +1,7 @@
 (herald "Function constraint test protocol"
   (comment "Skeletons 2, 4, and 7 should have no shapes."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from fnof_test.scm")
 
 (defprotocol fnoftest basic
diff --git a/tst/fnof_woolam.tst b/tst/fnof_woolam.tst
--- a/tst/fnof_woolam.tst
+++ b/tst/fnof_woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol, using fnof to emulate ltk function")
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from fnof_woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/fnof_yahalom.tst b/tst/fnof_yahalom.tst
--- a/tst/fnof_yahalom.tst
+++ b/tst/fnof_yahalom.tst
@@ -2,7 +2,7 @@
   "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function"
   (bound 12))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from fnof_yahalom.scm")
 
 (defprotocol yahalom basic
diff --git a/tst/goals.tst b/tst/goals.tst
--- a/tst/goals.tst
+++ b/tst/goals.tst
@@ -1,6 +1,6 @@
 (herald goals)
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from goals.scm")
 
 (defprotocol ns basic
@@ -108,7 +108,7 @@
   (parent 2)
   (unrealized)
   (shape)
-  (satisfies (no (b b) (n1 n1) (z0 0)))
+  (satisfies yes)
   (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
   (origs (n1 (0 0))))
 
diff --git a/tst/iadh_um.tst b/tst/iadh_um.tst
# file too large to diff: tst/iadh_um.tst
diff --git a/tst/injection.tst b/tst/injection.tst
--- a/tst/injection.tst
+++ b/tst/injection.tst
@@ -2,7 +2,7 @@
   (comment "This protocol contains a man-in-the-middle"
     "attack discovered by Galvin Lowe."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from injection.scm")
 
 (defprotocol ns diffie-hellman
diff --git a/tst/kerb.tst b/tst/kerb.tst
--- a/tst/kerb.tst
+++ b/tst/kerb.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from kerb.scm")
 
 (defprotocol kerb-flawed basic
diff --git a/tst/kerberos++.tst b/tst/kerberos++.tst
--- a/tst/kerberos++.tst
+++ b/tst/kerberos++.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from kerberos++.scm")
 
 (defprotocol kerberos basic
diff --git a/tst/lt_test.tst b/tst/lt_test.tst
--- a/tst/lt_test.tst
+++ b/tst/lt_test.tst
@@ -2,7 +2,7 @@
   (comment "First and third skeletons should have a shape,"
     "second and fourth should be dead."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from lt_test.scm")
 
 (defprotocol lttest basic
diff --git a/tst/neq_test.tst b/tst/neq_test.tst
--- a/tst/neq_test.tst
+++ b/tst/neq_test.tst
@@ -2,7 +2,7 @@
   (comment "First skeleton should have a shape,"
     "second, and hird should be dead."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from neq_test.scm")
 
 (defprotocol neqtest basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -2,7 +2,7 @@
   (comment "This protocol contains a man-in-the-middle"
     "attack discovered by Galvin Lowe."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from ns.scm")
 
 (defprotocol ns basic
diff --git a/tst/or.tst b/tst/or.tst
--- a/tst/or.tst
+++ b/tst/or.tst
@@ -1,7 +1,7 @@
 (herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg"))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from or.scm")
 
 (defprotocol or basic
diff --git a/tst/owang.tst b/tst/owang.tst
--- a/tst/owang.tst
+++ b/tst/owang.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from owang.scm")
 
 (defprotocol wang basic
diff --git a/tst/owat.tst b/tst/owat.tst
--- a/tst/owat.tst
+++ b/tst/owat.tst
@@ -1,7 +1,7 @@
 (herald "One-way Authentication Test with bltk keys"
   (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from owat.scm")
 
 (defprotocol owa diffie-hellman
diff --git a/tst/pkinit.tst b/tst/pkinit.tst
--- a/tst/pkinit.tst
+++ b/tst/pkinit.tst
@@ -1,6 +1,6 @@
 (herald "Kerberos PKINIT")
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from pkinit.scm")
 
 (defprotocol pkinit-flawed basic
diff --git a/tst/plaindh.tst b/tst/plaindh.tst
--- a/tst/plaindh.tst
+++ b/tst/plaindh.tst
@@ -1,7 +1,7 @@
 (herald "Plain diffie-hellman protocol with challenge-response"
   (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from plaindh.scm")
 
 (defprotocol plaindh diffie-hellman
diff --git a/tst/priority_test.tst b/tst/priority_test.tst
--- a/tst/priority_test.tst
+++ b/tst/priority_test.tst
@@ -1,6 +1,6 @@
 (herald "Receive priority test protocol")
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from priority_test.scm")
 
 (defprotocol priority_test basic
diff --git a/tst/reflect.tst b/tst/reflect.tst
--- a/tst/reflect.tst
+++ b/tst/reflect.tst
@@ -1,6 +1,6 @@
 (herald reflect)
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from reflect.scm")
 
 (defprotocol reflect basic
diff --git a/tst/staticdh.tst b/tst/staticdh.tst
--- a/tst/staticdh.tst
+++ b/tst/staticdh.tst
@@ -1,6 +1,6 @@
 (herald "Static DH key exchange" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from staticdh.scm")
 
 (defprotocol staticdh1 diffie-hellman
diff --git a/tst/station.tst b/tst/station.tst
--- a/tst/station.tst
+++ b/tst/station.tst
@@ -1,6 +1,6 @@
 (herald "Station-to-station protocol" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from station.scm")
 
 (defprotocol station-to-station diffie-hellman
diff --git a/tst/station2.tst b/tst/station2.tst
--- a/tst/station2.tst
+++ b/tst/station2.tst
@@ -1,6 +1,6 @@
 (herald "Station-to-station protocol" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from station2.scm")
 
 (defprotocol station-to-station diffie-hellman
diff --git a/tst/subsort_test.tst b/tst/subsort_test.tst
--- a/tst/subsort_test.tst
+++ b/tst/subsort_test.tst
@@ -2,7 +2,7 @@
   (comment "First, third, and fourth skeletons should have a shape,"
     "second should be dead."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from subsort_test.scm")
 
 (defprotocol subsorttest basic
diff --git a/tst/test_small.tst b/tst/test_small.tst
--- a/tst/test_small.tst
+++ b/tst/test_small.tst
@@ -1,6 +1,6 @@
 (herald "small test" (algebra diffie-hellman))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from test_small.scm")
 
 (defprotocol test diffie-hellman
diff --git a/tst/unilateral.tst b/tst/unilateral.tst
--- a/tst/unilateral.tst
+++ b/tst/unilateral.tst
@@ -1,6 +1,6 @@
 (herald unilateral)
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from unilateral.scm")
 
 (defprotocol unilateral basic
diff --git a/tst/uniq-gen-test.tst b/tst/uniq-gen-test.tst
--- a/tst/uniq-gen-test.tst
+++ b/tst/uniq-gen-test.tst
@@ -1,7 +1,7 @@
 (herald "Unique generation test protocols."
   (comment "Skeletons 2, 4, and 7 should have no shapes."))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from uniq-gen-test.scm")
 
 (defprotocol uniqgentest basic
diff --git a/tst/woolam.tst b/tst/woolam.tst
--- a/tst/woolam.tst
+++ b/tst/woolam.tst
@@ -1,6 +1,6 @@
 (herald "Woo-Lam Protocol")
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from woolam.scm")
 
 (defprotocol woolam basic
diff --git a/tst/wrap_decrypt.tst b/tst/wrap_decrypt.tst
--- a/tst/wrap_decrypt.tst
+++ b/tst/wrap_decrypt.tst
@@ -1,6 +1,6 @@
 (herald wrap-decrypt (bound 10))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from wrap_decrypt.lsp")
 (comment "Strand count bounded at 10")
 
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,7 +1,7 @@
 (herald "Yahalom Protocol with Forwarding Removed"
   (algebra diffie-hellman) (bound 12))
 
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.1")
 (comment "All input read from yahalom.scm")
 
 (defprotocol yahalom diffie-hellman