diff git a/docs/manual.tex b/docs/manual.tex
index 395f29c25b1a72ce4074ae1ab3c3c6660219f0a0..73258e96dc8e0311e2139976c98eb96cacf7d75f 100644
 a/docs/manual.tex
+++ b/docs/manual.tex
@@ 745,13 +745,13 @@ e.g., determinism, postconditions, specifications,
so that they are not tested:
\begin{itemize}
\item
If there is a proof file \code{proof$M$$f$IsDeterministic.*},
+If there is a proof file \code{proof$M$$f$IsDeterministic.*},
a determinism annotation for operation $M.f$ is not tested.
\item
If there is a proof file \code{proof$M$$f$SatisfiesPostCondition.*},
+If there is a proof file \code{proof$M$$f$SatisfiesPostCondition.*},
a postcondition for operation $M.f$ is not tested.
\item
If there is a proof file \code{proof$M$$f$SatisfiesSpecification.*},
+If there is a proof file \code{proof$M$$f$SatisfiesSpecification.*},
a specification for operation $M.f$ is not tested.
\end{itemize}
Note that the file suffix and all nonalphanumberic characters
diff git a/examples/equivalent_operations/BacciEtAl12.curry b/examples/equivalent_operations/BacciEtAl12.curry
new file mode 100644
index 0000000000000000000000000000000000000000..f3139a259e2a2ec4d2ab92394beb0ab502cbbe4c
 /dev/null
+++ b/examples/equivalent_operations/BacciEtAl12.curry
@@ 0,0 +1,46 @@
+import Test.Prop
+
+ This is an example from
+
+ G. Bacci, M. Comini, M.A. Feliu, A. Villanueva:
+ Automatic Synthesis of Specifications for First Order Curry
+ Proc. Principles and Practice of Declarative Programming (PPDP'12),
+ ACM Press, pp. 2534
+
+ It shows that two operations, which compute the same values,
+ might compute different results in larger contexts.
+ This example is also used in the introduction of the paper
+ explaining the equivalence checking features implemented in CurryCheck:
+
+ Antoy, S., Hanus, M.:
+ Equivalence Checking of Nondeterministic Operations
+ Proc. 14th Int. Symp. on Functional and Logic Programming (FLOPS 2018),
+ Springer LNCS 10818, pp. 149165, 2018
+
+data AB = A  B
+ deriving (Eq,Show)
+
+data C = C AB
+ deriving (Eq,Show)
+
+h :: AB > AB
+h A = A
+
+f :: AB > C
+f x = C (h x)
+
+g :: AB > C
+g A = C A
+
+
+ The computed result equivalence of f and g on ground values
+ always holds, i.e., f and g always compute same values.
+ Since the domain is finite, this property is actually proved by CurryCheck.
+f_and_g :: AB > Prop
+f_and_g x = f x <~> g x
+
+ The contextual equivalence of f and g does not hold.
+ The counterexample is found by CurryCheck with the 2nd test
+ (or with the 1st test when option "equivalence=autoselect" is used).
+f_equiv_g :: Prop
+f_equiv_g = f <=> g
diff git a/examples/equivalent_operations/Intersperse.curry b/examples/equivalent_operations/Intersperse.curry
index 1d93da8056eaf011a56f47a639e4390b21dc255a..8b458d13ff26ea85303ac8ea772210a1fec63e3d 100644
 a/examples/equivalent_operations/Intersperse.curry
+++ b/examples/equivalent_operations/Intersperse.curry
@@ 22,5 +22,11 @@ intersperse2 sep (x:xs) = x : go xs
go (y:ys) = sep : y : go ys
 These operations are not equivalent:
+ These operations are not equivalent (falsified by 43th test):
intersperseEquiv = intersperse1 <=> intersperse2
+
+ These operations are not equivalent (falsified by 4th test):
+intersperseEquiv'TERMINATE = intersperse1 <=> intersperse2
+
+ Ground equivalence testing is successful:
+intersperseEquiv'GROUND x xs = intersperse1 x xs <~> intersperse2 x xs
diff git a/examples/equivalent_operations/Ints12.curry b/examples/equivalent_operations/Ints12.curry
index 4ea999b384b3ef1689a9965c38a48f20885c60ca..c47a4e4045dd8faaedaeb47a526fe5e1d09b565a 100644
 a/examples/equivalent_operations/Ints12.curry
+++ b/examples/equivalent_operations/Ints12.curry
@@ 1,6 +1,5 @@
 Testing the equivalence of nonterminating operations:
import Data.Nat
import Test.Prop
 Two different infinite lists:
diff git a/examples/equivalent_operations/NDInsert.curry b/examples/equivalent_operations/NDInsert.curry
index 2c2ac43c3cf34fe974e3faad4bf0b44399d583be..4fcc493a34eeb379cc89fea320f7159a50488f35 100644
 a/examples/equivalent_operations/NDInsert.curry
+++ b/examples/equivalent_operations/NDInsert.curry
@@ 23,3 +23,6 @@ ndinsert_groundequiv x xs = ndinsert1 x xs <~> ndinsert2 x xs
 In PAKCS, the counter example is reported by the 7th test:
ndinsert_equiv = ndinsert1 <=> ndinsert2
+ With termination info, the counter example is reported by the 1st test:
+ndinsert_equiv'TERMINATE = ndinsert1 <=> ndinsert2
+
diff git a/examples/equivalent_operations/Perm.curry b/examples/equivalent_operations/Perm.curry
new file mode 100644
index 0000000000000000000000000000000000000000..4118d21b48eba9c5eb72dc16fdbe29fc79bce6e9
 /dev/null
+++ b/examples/equivalent_operations/Perm.curry
@@ 0,0 +1,30 @@
+import Test.Prop
+
+ Definition of permute from library Combinatorial
+ Note that this definition is "spine strict", i.e., it does not return
+ any partial value for partial lists, e.g.,
+ head (permute (1:failed)) > no value!
+permute :: [a] > [a]
+permute [] = []
+permute (x:xs) = ndinsert (permute xs)
+ where ndinsert [] = [x]
+ ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
+
+ An alternative, less strict definition of permutations, e.g.,
+ head (perm (1:failed)) > 1
+perm :: [a] > [a]
+perm [] = []
+perm (x:xs) = ndinsert x (perm xs)
+ where ndinsert x ys = x : ys
+ ndinsert x (y:ys) = y : ndinsert x ys
+
+
+
+ Equivalence falsified by 13th test:
+permEquiv = perm <=> permute
+
+ Equivalence falsified by 3rd test:
+permEquiv'TERMINATE = perm <=> permute
+
+ Ground equivalence not falsified:
+permEquiv'GROUND xs = perm xs <~> permute xs
diff git a/examples/equivalent_operations/README.md b/examples/equivalent_operations/README.md
index cc8957d15315cb8d6ce3dffc24919070fc39d628..84f7d91f1c6fe0e9489a90a2ade93b778f4df2aa 100644
 a/examples/equivalent_operations/README.md
+++ b/examples/equivalent_operations/README.md
@@ 1,15 +1,20 @@
+Equivalence checking with CurryCheck
+====================================
+
This directory contains some examples for the use
of CurryCheck to check the equivalence of operations.
Since most of these are examples to test whether CurryCheck
is able to report counterexamples, their test fails intentionally.
These are the programs
+ BacciEtAl12 (simple example from Bacci et al PPDP'12)
 Intersperse (inserting separators in a list [Christiansen/Seidel'11])
 Ints12 (generators for infinite lists)
 NDInsert (nondeterministic list insertion)
+ Perm (permutation from library Combinatorial vs. less strict version)
 RevRev (double reverse)
 SimpleExample
 SortEquiv (two variants of permutation sort)
+ SortPermute (two variants of permutation sort with a stricter permutation)
 Take (two variants of take [Foner/Zhang/Lampropoulos'18])
 Unzip (two variants of unzip [Chitil'11])
diff git a/examples/equivalent_operations/RevRev.curry b/examples/equivalent_operations/RevRev.curry
index ff84210fc271469e21f1a4a5d7ea155cc58dc987..006add786c8cf22b167b1571b0f29c378dc8ad64 100644
 a/examples/equivalent_operations/RevRev.curry
+++ b/examples/equivalent_operations/RevRev.curry
@@ 6,4 +6,12 @@ revrev xs = reverse (reverse xs)
 Test: is double reverse equivalent to the identity?
 This is not the case if both are applied to the context
 head (... (1:failed))
+
+ Equivalence falsified by 13th test:
+revrevid = revrev <=> id
+
+ Equivalence falsified by 3rd test:
revrevid'TERMINATE = revrev <=> id
+
+ Ground equivalence not falsified:
+revrevid'GROUND xs = revrev xs <~> id xs
diff git a/examples/equivalent_operations/SimpleExample.curry b/examples/equivalent_operations/SimpleExample.curry
deleted file mode 100644
index fdc22db66569478c11299bcb50bb07db95c9afee..0000000000000000000000000000000000000000
 a/examples/equivalent_operations/SimpleExample.curry
+++ /dev/null
@@ 1,27 +0,0 @@
import Test.Prop

 This is an example which shows the "nonreferentiality" of Curry (according
 to [Bacci et al. PPDP'12]), i.e., it shows that two operations, which
 compute the same values, might compute different results in larger
 contexts:

data AB = A  B
 deriving (Eq,Show)

data C = C AB
 deriving (Eq,Show)

h A = A

g x = C (h x)

g' A = C A


 The computed result equivalence of g and g' on ground values
 always holds, i.e., g and g' always compute same values:
g_and_g' :: AB > Prop
g_and_g' x = g x <~> g' x

 The contextual equivalence of g and g' does not hold:
g_equiv_g' = g <=> g'
diff git a/examples/equivalent_operations/SortPermute.curry b/examples/equivalent_operations/SortPermute.curry
new file mode 100644
index 0000000000000000000000000000000000000000..ed4bbbc89bd85678abda751fdbeb6f27372b5c51
 /dev/null
+++ b/examples/equivalent_operations/SortPermute.curry
@@ 0,0 +1,42 @@
+import Test.Prop
+
+ Definition of permute from library `Combinatorial` (part of PAKCS
+ distribution up to version 2.0.2 and contained in Curry package
+ `combinatorial` version 1.0.0).
+
+ Note that this definition is "spine strict", i.e., it does not return
+ any partial value for partial lists, e.g.,
+ head (permute (1:failed)) > no value!
+permute :: [a] > [a]
+permute [] = []
+permute (x:xs) = ndinsert (permute xs)
+ where ndinsert [] = [x]
+ ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
+
+
+
+sorted :: Ord a => [a] > Bool
+sorted [] = True
+sorted [_] = True
+sorted (x:y:zs) = x<=y && sorted (y:zs)
+
+psort :: Ord a => [a] > [a]
+psort xs  sorted ys = ys where ys = permute xs
+
+
+
+idSorted :: Ord a => [a] > [a]
+idSorted [] = []
+idSorted [x] = [x]
+idSorted (x:y:zs)  x<=y = x : idSorted (y:zs)
+
+isort :: Ord a => [a] > [a]
+isort xs = idSorted (permute xs)
+
+
+
+ Equivalence falsified by 1174th test:
+equiv = psort <=> (isort :: [Int] > [Int])
+
+ Equivalence falsified by 46th test:
+equiv'TERMINATE = psort <=> (isort :: [Int] > [Int])
diff git a/examples/equivalent_operations/Take.curry b/examples/equivalent_operations/Take.curry
index b13abfbf747e1a5f951026b98480e47fab538ff6..0aede3d861878929a6dfc925cd78913c2745d442 100644
 a/examples/equivalent_operations/Take.curry
+++ b/examples/equivalent_operations/Take.curry
@@ 1,7 +1,7 @@
 Example to show the nonequivalence of two versions of the
 `take` operation, taken from

 Foner, K. and Zhang, H. and Lampropoulos, L.: {Keep Your Laziness in Check
+ Foner, K. and Zhang, H. and Lampropoulos, L.: Keep Your Laziness in Check
 ICFP 2018,
 DOI: 10.1145/3236797
@@ 27,5 +27,8 @@ take_groundequiv x xs = take1 x xs <~> take2 x xs
 by evaluating `take... failed [])` or `take... 0 failed`.
 Thus, we check the equivalence with CurryCheck:
 In PAKCS, the counter example is reported by the 11th test:
+ Equivalence is falsified by the 11th test:
take_equiv = take1 <=> take2
+
+ With termination information, equivalence is falsified by the 2nd test:
+take_equiv'TERMINATE = take1 <=> take2
diff git a/examples/equivalent_operations/Unzip.curry b/examples/equivalent_operations/Unzip.curry
index 032d2a5499b3adf83f8dc11c43a5357fa6e15ed7..b4a03741d56ebf1c1fa0a6097a8f0291d9527bfc 100644
 a/examples/equivalent_operations/Unzip.curry
+++ b/examples/equivalent_operations/Unzip.curry
@@ 14,7 +14,13 @@ unzip1 ((x,y):ps) = (x:xs,y:ys) where (xs,ys) = unzip1 ps
 Definition from Chitil'11:
unzip2 :: [(a,b)] > ([a],[b])
unzip2 xs = foldr (\(a,b) (as,bs) > (a:as,b:bs)) ([],[]) xs
+unzip2 xs = foldr (\ (a,b) (as,bs) > (a:as,b:bs)) ([],[]) xs
 These operations are not equivalent:
+ Equivalence falsified by 27th test:
unzipEquiv = unzip1 <=> unzip2
+
+ Equivalence falsified by 6th test:
+unzipEquiv'TERMINATE = unzip1 <=> unzip2
+
+ Ground equivalence is not falsified:
+unzipEquiv'GROUND xs = unzip1 xs <~> unzip2 xs
diff git a/package.json b/package.json
index 37ae2b29cf4c2e429a2077a8aaff03b729924773..50324a526abcdea16c796b7fa4cd19b14e9a5b5d 100644
 a/package.json
+++ b/package.json
@@ 15,15 +15,14 @@
"easycheck" : ">= 0.0.1",
"flatcurry" : ">= 2.0.0",
"frontendexec" : ">= 0.0.1",
 "peano" : ">= 1.0.0",
"profiling" : ">= 1.0.0",
"rewriting" : ">= 2.0.0",
"setfunctions" : ">= 0.0.1",
"wlpprint" : ">= 0.0.1"
},
"compilerCompatibility": {
 "pakcs": ">= 2.0.0",
 "kics2": ">= 2.0.0"
+ "pakcs": ">= 2.0.0, < 3.0.0",
+ "kics2": ">= 2.0.0, < 3.0.0"
},
"configModule": "CC.Config",
"executable": {