diff --git a/README.md b/README.md
index a2fe509..9b21666 100644
--- a/README.md
+++ b/README.md
@@ -21,6 +21,21 @@ I decided to implement a new domain / sort. It will be an order domain, with bot
 Milestones: [x] - completed, [#] - finishing (75%-95%), [+] - in the middle (25%-75%), [-] - just started (5%-25%), [_] - not started.
 
 Goals -- version targets may be reassigned:
+- [-] New sort: order. (v2.1)
+- [#] Order sort example: binomial heap. (v2.1)
+- [ ] Datatype-level invariants shared by all constructors of a datatype. (v2.1)
+- [ ] Solver directives in .gadt source code -- exposing the options available from the command-line interface. (v2.1)
+- [ ] Or-patterns `p1 | p2` introducing disjunctions in premises, either eliminated by disjunction elimination or expanded by implication clause duplication -- depending on user-level option; preserved in exported code. (v2.1)
+- [ ] Meta-automatic mode: retry with modified user-level parameter settings if inference fails. (v2.2)
+- [ ] Improve error reporting (likely culprit). (v2.2)
+- [ ] Ability to parse `.gadti` and `.mli` files, and use them with the module access `open M`, `let open M in ...`, `M.(...)` and `M.x` syntaxes. (v2.3)
+- [ ] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v2.3)
+- [ ] Optimize, paying attention to the speed of the update mode. (v2.3)
+- [ ] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v2.4)
+- [ ] More general `when` clauses for patterns. Factorize `Num` and `NumAdd` out of the `expr` type. (v2.4)
+- [ ] Add a new "promising" sort. Candidates: proper integer numbers, ring of polynomials... (v2.4)
+
+Version 2.0 milestones are now completed:
 - [x] Export to OCaml using built-in or pervasives OCaml types, in particular `bool` instead of `boolean`. (v1.1)
 - [x] Support source code comments preserved in the AST. (v1.1)
 - [x] Factorize to make extending and adding sorts easier. (v1.2)
@@ -32,21 +47,8 @@ Goals -- version targets may be reassigned:
 - [x] Flagship example: AVL tree from OCaml standard library (height imbalance limited by 2). (v1.2)
 - [x] Option to detect all dead code. (v1.2.1)
 - [x] Improve coverage for examples from Chuan-kai Lin's PhD thesis. (v2.0)
-- [#] Improve coverage for DML / Liquid Types examples. (v2.0)
+- [x] Improve coverage for DML / Liquid Types examples. (v2.0)
 - [x] if-then-else syntax. (v2.0)
-- [-] New sort: order. (v2.1)
-- [#] Order sort example: binomial heap. (v2.1)
-- [ ] Datatype-level invariants shared by all constructors of a datatype. (v2.1)
-- [ ] Solver directives in .gadt source code -- exposing the options available from the command-line interface. (v2.1)
-- [ ] Or-patterns `p1 | p2` introducing disjunctions in premises, either eliminated by disjunction elimination or expanded by implication clause duplication -- depending on user-level option; preserved in exported code. (v2.1)
-- [ ] Meta-automatic mode: retry with modified user-level parameter settings if inference fails. (v2.1)
-- [ ] Ability to parse `.gadti` and `.mli` files, and use them with the module access `open M`, `let open M in ...`, `M.(...)` and `M.x` syntaxes. (v2.2)
-- [ ] Improve error reporting (likely culprit). (v2.2)
-- [ ] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v2.2)
-- [ ] Optimize, paying attention to the speed of the update mode. (v2.2)
-- [ ] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v2.2)
-- [ ] More general `when` clauses for patterns. Factorize `Num` and `NumAdd` out of the `expr` type. (v2.3)
-- [ ] Add a new "promising" sort. Candidates: proper integer numbers, ring of polynomials... (v2.4)
 
 Version 1.0 milestones are now completed:
 - [x] Setup project. Parse and pretty-print.
diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf
index 20eaa46..61a7ffb 100644
Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ
diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
index aad402e..0bdc55c 100644
--- a/doc/invargent-manual.tm
+++ b/doc/invargent-manual.tm
@@ -13,13 +13,13 @@
   to type systems that deal with data-types. Type systems with GADTs
   introduce the ability to reason about return type by case analysis of the
   input value, while keeping the benefits of a simple semantics of types, for
-  example deciding equality can be very simple. Existential types hide some
-  information conveyed in a type, usually when that information cannot be
-  reconstructed in the type system. A part of the type will often fail to be
-  expressible in the simple language of types, when the dependence on the
-  input to the program is complex. GADTs express existential types by using
-  local type variables for the hidden parts of the type encapsulated in a
-  GADT.
+  example deciding equality between types can be very simple. Existential
+  types hide some information conveyed in a type, usually when that
+  information cannot be reconstructed in the type system. A part of the type
+  will often fail to be expressible in the simple language of types, when the
+  dependence on the input to the program is complex. GADTs express
+  existential types by using local type variables for the hidden parts of the
+  type encapsulated in a GADT.
 
   The InvarGenT type system for GADTs differs from more pragmatic approaches
   in mainstream functional languages in that we do not require any type
@@ -67,7 +67,7 @@
   In examples here we use Unicode characters. For ASCII equivalents, take a
   quick look at the tables in the following section.
 
-  We start simple, with a function that can compute a value from a
+  We start with a simple example, a function that can compute a value from a
   representation of an expression -- a ready to use value whether it be
   <verbatim|Int> or <verbatim|Bool>. Prior to the introduction of GADT types,
   we could only implement a function <verbatim|eval : <math|\<forall\>>a.
@@ -145,21 +145,22 @@
   The syntax <verbatim|external let> allows us to name an OCaml library
   function or give an OCaml definition which we opt-out from translating to
   InvarGenT. Such a definition will be verified against the rest of the
-  program when InvarGenT calls <verbatim|ocamlc -c> (or Haskell in the
-  future) to verify the exported code. Another variant of <verbatim|external>
-  (omitting the <verbatim|let> keyword) exports a value using
-  <verbatim|external> in OCaml code, which is OCaml source declaration of the
-  foreign function interface of OCaml. When we are not interested in linking
-  and running the exported code, we can omit the part starting with the
-  <verbatim|=> sign. The exported code will reuse the name in the FFI
-  definition: <verbatim|external f : >...<verbatim| = "f">.
-
-  The type inferred is <verbatim|eval : <math|\<forall\>>a. Term
-  a<math|\<rightarrow\>>a>. GADTs make it possible to reveal that
-  <verbatim|IsZero x> is a <verbatim|Term Bool> and therefore the result of
-  <verbatim|eval> should in its case be <verbatim|Bool>, <verbatim|Plus (x,
-  y)> is a <verbatim|Term Num> and the result of <verbatim|eval> should in
-  its case be <verbatim|Num>, etc. The <verbatim|if/eif<math|\<ldots\>>then<math|\<ldots\>>else<math|\<ldots\>>>
+  program when InvarGenT calls <verbatim|ocamlc -c> to verify the exported
+  code. Another variant of <verbatim|external> (omitting the <verbatim|let>
+  keyword) exports a value using <verbatim|external> in OCaml code, which is
+  OCaml source declaration of the foreign function interface of OCaml. When
+  we are not interested in linking and running the exported code, we can omit
+  the part starting with the <verbatim|=> sign. The exported code will reuse
+  the name in the FFI definition: <verbatim|external f : >...<verbatim| =
+  "f">.
+
+  The type inferred for the above example is <verbatim|eval :
+  <math|\<forall\>>a. Term a<math|\<rightarrow\>>a>. GADTs make it possible
+  to reveal that <verbatim|IsZero x> is a <verbatim|Term Bool> and therefore
+  the result of <verbatim|eval> should in its case be <verbatim|Bool>,
+  <verbatim|Plus (x, y)> is a <verbatim|Term Num> and the result of
+  <verbatim|eval> should in its case be <verbatim|Num>, etc. The
+  <verbatim|if/eif<math|\<ldots\>>then<math|\<ldots\>>else<math|\<ldots\>>>
   syntax is a syntactic sugar for <verbatim|match<math|/>ematch
   <math|\<ldots\>> with True -\<gtr\> <math|\<ldots\>> \| False -\<gtr\>
   <math|\<ldots\>>>, and any such expressions are exported using
@@ -427,15 +428,14 @@
 
   We get <verbatim|filter<math|:\<forall\>>n,
   a.(a<math|\<rightarrow\>>Bool)<math|\<rightarrow\>>List (a,
-  n)<math|\<rightarrow\>> <math|\<exists\>>k[0<math|\<leq\>>n
-  <math|\<wedge\>> 0<math|\<leq\>>k <math|\<wedge\>> k<math|\<leq\>>n].List
-  (a, k)>. Note that we need to use both <verbatim|efunction> and
-  <verbatim|eif> above, since every use of <verbatim|function>,
-  <verbatim|match> or <verbatim|if> will force the types of its branches to
-  be equal. In particular, for lists with length the resulting length would
-  have to be the same in each branch. If the constraint cannot be met, as for
-  <verbatim|filter> with either <verbatim|function> or <verbatim|if>, the
-  code will not type-check.
+  n)<math|\<rightarrow\>> <math|\<exists\>>k[0<math|\<leq\>>k
+  <math|\<wedge\>> k<math|\<leq\>>n].List (a, k)>. Note that we need to use
+  both <verbatim|efunction> and <verbatim|eif> above, since every use of
+  <verbatim|function>, <verbatim|match> or <verbatim|if> will force the types
+  of its branches to be equal. In particular, for lists with length the
+  resulting length would have to be the same in each branch. If the
+  constraint cannot be met, as for <verbatim|filter> with either
+  <verbatim|function> or <verbatim|if>, the code will not type-check.
 
   A more complex example that computes bitwise <em|or> -- <verbatim|ub>
   stands for ``upper bound'':
@@ -617,6 +617,11 @@
   test>|<cell|<verbatim|let rec f =>...<verbatim| test e1; >...<verbatim|;
   en>>>>>>
 
+  Toplevel non-recursive <verbatim|let> definitions are polymorphic as an
+  exception. In expressions, <verbatim|let<math|\<ldots\>>in> definitions are
+  monomorphic, one should use the <verbatim|let rec<math|\<ldots\>>in> syntax
+  to get a polymorphic <verbatim|let>-binding.
+
   Tests list expressions of type <verbatim|Bool> that at runtime have to
   evaluate to <verbatim|True>. Type inference is affected by the constraints
   generated to typecheck the expressions.
@@ -693,20 +698,20 @@
   <verbatim|-inform> option:
 
   <\code>
-    $ ./invargent -inform examples/binomial_heap_nonrec.gadt
+    $ ./invargent -inform examples/avl_tree.gadt
   </code>
 
-  In some situations, hopefully unlikely for simple programs, the default
-  parameters of the solver algorithms do not suffice. Consider this example,
-  where we use <verbatim|-full_annot> to generate type annotations on
-  <verbatim|function> and <verbatim|let>..<verbatim|in> nodes in the
-  <verbatim|.ml> file, in addition to annotations on <verbatim|let rec>
-  nodes:
+  Below we demonstrate what happens with insufficiently high parameter
+  setting. Consider this example, where we use <verbatim|-full_annot> to
+  generate type annotations on <verbatim|function> and
+  <verbatim|let>..<verbatim|in> nodes in the <verbatim|.ml> file, in addition
+  to annotations on <verbatim|let rec> nodes:
 
   <\code>
-    $ ./invargent -inform -full_annot examples/equal_assert.gadt
+    $ ./invargent -inform -term_abduction_timeout 100
+    examples/equal_assert.gadt
 
-    File "examples/equal_assert.gadt", line 20, characters 5-103:
+    File "examples/equal_assert.gadt", line 19, characters 24-38:
 
     No answer in type: term abduction failed
 
@@ -720,24 +725,7 @@
   The <verbatim|Perhaps increase> suggestions are generated only when the
   corresponding limit has actually been exceeded. Remember however that the
   limits will often be exceeded for erroneus programs which should not
-  type-check. Here the default number of steps till term abduction timeout,
-  which is just <verbatim|700> to speed up failing for actually erroneous
-  programs, is too low. The complete output with timeout increased:
-
-  <\code>
-    $ ./invargent -inform -full_annot -term_abduction_timeout 4000 \\
-    examples/<no-break>equal_assert.gadt
-
-    val equal : <math|\<forall\>>a, b. (Ty a, Ty b) <math|\<rightarrow\>> a
-    <math|\<rightarrow\>> b <math|\<rightarrow\>> Bool
-
-    InvarGenT: Generated file examples/equal_assert.gadti
-
-    InvarGenT: Generated file examples/equal_assert.ml
-
-    InvarGenT: Command "ocamlc -c examples/equal_assert.ml" exited with code
-    0
-  </code>
+  type-check.
 
   To understand the intent of the solver parameters, we need a rough
   ``birds-eye view'' understanding of how InvarGenT works. The invariants and
@@ -746,9 +734,9 @@
   computations are traditional tools used for solving recursive equations
   over an ordered structure. In case of implicational constraints that are
   generated for type inference with GADTs, constraint abduction is a form of
-  LUB computation. <em|Disjunction elimination> is our term for computing the
-  GLB wrt. strength for formulas that are conjunctions of atoms. We want the
-  invariants of recursive definitions -- i.e. the types of recursive
+  LUB computation. <em|Constraint generalization> is our term for computing
+  the GLB wrt. strength for formulas that are conjunctions of atoms. We want
+  the invariants of recursive definitions -- i.e. the types of recursive
   functions and formulas constraining their type variables -- to be as weak
   as possible, to make the use of the corresponding definitions as easy as
   possible. The weaker the invariant, the more general the type of
@@ -757,7 +745,7 @@
   <verbatim|efunction> expressions and formulas constraining their type
   variables -- we want the strongest possible solutions, because stronger
   postcondition provides more information at use sites of a definition.
-  Therefore we use GLB, disjunction elimination, but only if existential
+  Therefore we use GLB, constraint generalization, but only if existential
   types have been introduced by <verbatim|efunction> or <verbatim|ematch>.
 
   Below we discuss all of the InvarGenT options.
@@ -845,7 +833,8 @@
     equation or inequality that does not conflict with other branches, but is
     equivalent to the conclusion equation/inequality. This parameter decides
     what range of coefficients is tried. If the highest coefficient in
-    correct answer is greater, abduction might fail.
+    correct answer is greater, abduction might fail. However, it often
+    succeeds because of other mechanisms used by the abduction algorithm.
 
     <item*|<verbatim|-num_prune_at>>Keep less than <math|N> elements in
     abduction sums (default 6). By elements here we mean distinct variables
@@ -1011,28 +1000,127 @@
     <verbatim|.ml> file.
   </description>
 
-  Let us see an example where a parameter allowing the solver do more search
-  is needed:
+  Let us have a look at test-suite examples that need a non-default parameter
+  setting.
+
+  <\code>
+    $ ./invargent -inform examples/non_pointwise_leq.gadt
+
+    File "examples/non_pointwise_leq.gadt", line 12, characters 14-60:
+
+    No answer in type: Answers do not converge
+
+    \;
+
+    Perhaps increase the -iterations_timeout parameter or try the
+    -more_existential option.
+
+    $ ./invargent -inform -prefer_guess examples/non_pointwise_leq.gadt
+
+    val leq : <math|\<forall\>>a. Nat a <math|\<rightarrow\>> NatLeq (a, a)
+
+    InvarGenT: Generated file examples/non_pointwise_leq.gadti
+
+    InvarGenT: Generated file examples/non_pointwise_leq.ml
+
+    InvarGenT: Command "ocamlc -w -25 -c examples/non_pointwise_leq.ml"
+    exited with code 0
+  </code>
+
+  Other examples that need the <verbatim|-prefer_guess> option:
+  <verbatim|non_pointwise_zip1_simpler.gadt>,
+  <verbatim|non_pointwise_zip1_simpler2.gadt>,
+  <verbatim|non_pointwise_zip1_modified.gadt>. On the other hand,
+  <verbatim|non_pointwise_zip1.gadt> is inferred with default settings.
 
   <\code>
-    $ ./invargent -inform -num_abduction_rotations 4
-    examples/flatten_quadrs.gadt
+    $ ./invargent -inform examples/liquid_heapsort_heapify_simpler.gadt
+
+    val heapify :
+
+    \ \ <math|\<forall\>>k, n, a[0 <math|\<leqslant\>> n <math|\<wedge\>> n +
+    1 <math|\<leqslant\>> k].
+
+    \ \ Num k <math|\<rightarrow\>> Array (a, k) <math|\<rightarrow\>> Num n
+    <math|\<rightarrow\>> ()
+
+    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.gadti
+
+    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.ml
+
+    InvarGenT: Command "ocamlc -w -25 -c examples/liquid_heapsort_heapify_simpler.ml"
+    exited with code 0
+
+    $ ./invargent -inform -prefer_bound_to_local \\
+    examples/liquid_heapsort_heapify_simpler.gadt
+
+    val heapify :
 
-    val flatten_quadrs :
+    \ \ <math|\<forall\>>i, k, n, a[0 <math|\<leqslant\>> n <math|\<wedge\>>
+    n + 1 <math|\<leqslant\>> i <math|\<wedge\>> i <math|\<leqslant\>> k].
 
-    \ \ <math|\<forall\>>n, a. List ((a, a, a, a), n) <math|\<rightarrow\>>
-    List (a, 4 n)
+    \ \ Num i <math|\<rightarrow\>> Array (a, k) <math|\<rightarrow\>> Num n
+    <math|\<rightarrow\>> ()
 
-    InvarGenT: Generated file examples/flatten_quadrs.gadti
+    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.gadti
 
-    InvarGenT: Generated file examples/flatten_quadrs.ml
+    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.ml
 
-    InvarGenT: Command "ocamlc -c examples/flatten_quadrs.ml" exited with
-    code 0
+    InvarGenT: Command "ocamlc -w -25 -c examples/liquid_heapsort_heapify_simpler.ml"
+    exited with code 0
   </code>
 
-  Based on user feedback, we will likely increase the default values of
-  parameters in a future version.
+  Above, the type inferred with default parameter setting is insufficiently
+  general. Other examples that need the <verbatim|-prefer_bound_to_local>
+  option: <verbatim|liquid_simplex_step_3a.gadt>,
+  <verbatim|liquid_simplex_step_6a_2.gadt>.
+
+  <\code>
+    $ ./invargent -inform examples/pointwise_zip2_harder.gadt
+
+    val zip2 : <math|\<forall\>>a, b. Zip2 (a, b) <math|\<rightarrow\>> a
+    <math|\<rightarrow\>> b
+
+    InvarGenT: Generated file examples/pointwise_zip2_harder.gadti
+
+    InvarGenT: Generated file examples/pointwise_zip2_harder.ml
+
+    File "examples/pointwise_zip2_harder.ml", line 19, characters 21-32:
+
+    Error: This kind of expression is not allowed as right-hand side of `let
+    rec'
+
+    InvarGenT: Command "ocamlc -w -25 -c examples/pointwise_zip2_harder.ml"
+    exited with code 2
+
+    InvarGenT: Regenerated file examples/pointwise_zip2_harder.ml
+
+    File "examples/pointwise_zip2_harder.ml", line 21, characters 21-32:
+
+    Error: This kind of expression is not allowed as right-hand side of `let
+    rec'
+
+    InvarGenT: Command "ocamlc -w -25 -c examples/pointwise_zip2_harder.ml"
+    exited with code 2
+
+    $ ./invargent -inform -no_ml examples/pointwise_zip2_harder.gadt
+
+    val zip2 : <math|\<forall\>>a, b. Zip2 (a, b) <math|\<rightarrow\>> a
+    <math|\<rightarrow\>> b
+
+    InvarGenT: Generated file examples/pointwise_zip2_harder.gadti
+  </code>
+
+  The example <verbatim|pointwise_zip2_harder.gadt> is not compatible with
+  the pass-by-value semantics. We can avoid the complaint of the OCaml
+  compiler by passing either the <verbatim|-no_ml> flag or the
+  <verbatim|-no_verif> flag. More interestingly, we can notice that the file
+  <verbatim|pointwise_zip2_harder.ml> is generated twice. This happens
+  because InvarGenT, noticing the failure, generates an OCaml source with
+  more type information, as if the <verbatim|-full_annot> option was used.
+
+  Unfortunately, inference fails for some examples regardless of parameters
+  setting. We discuss them in the next section.
 
   <section|Limitations of Current InvarGenT Inference>
 
@@ -1073,139 +1161,206 @@
   inference can incorporate heuristics for special cases, and can be modified
   to do a more exhaustive search.
 
-  The following example illustrates a limitation of our numerical abduction
-  algorithm that is not intrinsic to the numerical abduction problem. I.e. it
-  might be fixed by a smarter algorithm.
+  The example <verbatim|pointwise_head.gadt> fails because of the limitations
+  of the <verbatim|type> sort in representing disequalities.
 
   <\code>
-    datatype Elem
+    datatype Z
 
-    datatype List : num
+    datatype S : type
 
-    datacons LNil : List 0
+    datatype List : type * num
 
-    datacons LCons : <math|\<forall\>>n [0<math|\<leq\>>n]. Elem * List n
-    <math|\<longrightarrow\>> List (n+1)
+    datacons LNil : <math|\<forall\>>a. List(a, Z)
 
-    external length : <math|\<forall\>>n. List n <math|\<rightarrow\>> Num n
-    = "length"
+    datacons LCons : <math|\<forall\>>a, b. a * List(a, b)
+    <math|\<longrightarrow\>> List(a, S b)
 
     \;
 
-    let rec append =
+    let head = function
+
+    \ \ \| LCons (x, _) -\> x
 
-    \ \ function
+    \ \ \| LNil -\> assert false
+  </code>
 
-    \ \ \ \ \| LNil -\<gtr\>
+  If we omit the <verbatim|LNil> branch, we get the technically correct but
+  inadequate type <verbatim|<math|\<forall\>>a, b. List(a, b)
+  <math|\<rightarrow\>> a>, because the type system does not guarantee
+  exhaustiveness of the pattern matching. The intended type is
+  <verbatim|<math|\<forall\>>a, b. List(a, S b) <math|\<rightarrow\>> a>.
 
-    \ \ \ \ \ \ (function l when (length l + 1) \<less\>= 0 -\<gtr\> assert
-    false \| l -\<gtr\> l)
+  The example <verbatim|non_pointwise_fd_comp_harder.gadt> is inferred an
+  insufficiently general type <verbatim|<math|\<forall\>>a, b. FunDesc (b, b)
+  <math|\<rightarrow\>> FunDesc (b, a) <math|\<rightarrow\>> FunDesc (b, a)>.
 
-    \ \ \ \ \| LCons (x, xs) -\<gtr\>
+  <\code>
+    datatype FunDesc : type * type
 
-    \ \ \ \ \ \ (function l when (length l + 1) \<less\>= 0 -\<gtr\> assert
-    false
+    datacons FDI : <math|\<forall\>>a. FunDesc (a, a)
 
-    \ \ \ \ \ \ \| l -\<gtr\> LCons (x, append xs l))
-  </code>
+    datacons FDC : <math|\<forall\>>a, b. b <math|\<longrightarrow\>> FunDesc
+    (a, b)
 
-  The expected type is <verbatim|append : <math|\<forall\>>a, n,
-  k[0<math|\<leq\>>k]. List n<math|\<rightarrow\>>List
-  k<math|\<rightarrow\>>List (n+k)>. When our algorithm discovers that the
-  result is <math|n+k>, rather than <math|n>, it is already committed to
-  requiring that the result is no less than <math|1>. The answers on
-  successive iterations of the main algorithm do not converge: if the length
-  of the tail has to be at least one, then the length of the input list has
-  to be at least two, etc.
+    datacons FDG : <math|\<forall\>>a, b. (a <math|\<rightarrow\>> b)
+    <math|\<longrightarrow\>> FunDesc (a, b)
 
-  The following example is a natural variant of a function from the
-  <verbatim|avl_tree.gadt> example.
+    external fd_fun : <math|\<forall\>>a, b. FunDesc (a, b)
+    <math|\<rightarrow\>> a <math|\<rightarrow\>> b
 
-  <\code>
-    let rec add = fun x -\<gtr\> efunction
+    \;
 
-    \ \ \| Empty -\<gtr\> Node (Empty, x, Empty, 1)
+    let fd_comp fd1 fd2 =
 
-    \ \ \| Node (l, y, r, h) -\<gtr\>
+    \ \ let o f g x = f (g x) in
 
-    \ \ \ \ ematch compare x y with
+    \ \ match fd1 with
 
-    \ \ \ \ \| EQ -\<gtr\> Node (l, x, r, h)
+    \ \ \ \ \| FDI -\> fd2
 
-    \ \ \ \ \| LT -\<gtr\>
+    \ \ \ \ \| FDC b -\>\ 
 
-    \ \ \ \ \ \ let l' = add x l in
+    \ \ \ \ \ \ (match fd2 with
 
-    \ \ \ \ \ \ (ematch height l', height r with
+    \ \ \ \ \ \ \ \ \| FDI -\> fd1
 
-    \ \ \ \ \ \ \ \| hl', hr when hl' \<less\>= hr+2 -\<gtr\> create l' y r
+    \ \ \ \ \ \ \ \ \| FDC c -\> FDC (fd_fun fd2 b)
 
-    \ \ \ \ \ \ \ \| hl', hr when hr+3 \<less\>= hl' -\<gtr\> rotr l' y r)
+    \ \ \ \ \ \ \ \ \| FDG g -\> FDC (fd_fun fd2 b))
 
-    \ \ \ \ \| GT -\<gtr\>
+    \ \ \ \ \| FDG f -\>
 
-    \ \ \ \ \ \ let r' = add x r in
+    \ \ \ \ \ \ (match fd2 with
 
-    \ \ \ \ \ \ (ematch height r', height l with
+    \ \ \ \ \ \ \ \ \| FDI -\> fd1
 
-    \ \ \ \ \ \ \ \| hr', hl when hr' \<less\>= hl+2 -\<gtr\> create l y r'
+    \ \ \ \ \ \ \ \ \| FDC c -\> FDC c
 
-    \ \ \ \ \ \ \ \| hr', hl when hl+3 \<less\>= hr' -\<gtr\> rotl l y r')
+    \ \ \ \ \ \ \ \ \| FDG g -\> FDG (o (fd_fun fd2) f))
   </code>
 
-  The difference with the function in the <verbatim|avl_tree.gadt> file
-  amounts to computing <verbatim|height r>, resp. <verbatim|height l> near
-  the places where they are used. The inference fails because of lack of
-  sharing of information about <verbatim|l> due to facts about <verbatim|l' =
-  add x l>, resp. about <verbatim|r> due to facts about <verbatim|r' = add x
-  r>, with the other branch. The limits on information sharing between
-  pattern matching branches can also manifest in more mundane situations.
-  Compare for example the sources <verbatim|pointwise_extract.gadt> and
-  <verbatim|pointwise_extract2.gadt> from the examples directory. Type
-  inference fails for the latter example, which has functions as bodies of
-  pattern matching branches, rather than deconstructing a variable introduced
-  only once. More sophisticated algorithms might mitigate these shortcomings
-  in future versions of InvarGenT.
-
-  We end with an example where there is little hope of improvement. The
-  <verbatim|rotr> and <verbatim|rotl> functions in <verbatim|avl_tree.gadt>
-  use assertions to convey the preconditions. Ideally, we would like to be
-  able to simply write an implementation similar to the following one:
+  This happens because the second argument <verbatim|fd2> is not expanded
+  when <verbatim|fd1> is equal to <verbatim|FDI>. Type inference cannot carry
+  out the different reasoning steps leading to the more general type.
+
+  In the example <verbatim|liquid_bsearch2_harder4.gadt> it turns out to be
+  too hard to infer the full postcondition.
 
   <\code>
-    let rotr = fun l x r -\<gtr\>
+    datatype Array : type * num
+
+    external let array_make :
+
+    \ \ <math|\<forall\>>n, a [0<math|\<leqslant\>>n]. Num n
+    <math|\<rightarrow\>> a <math|\<rightarrow\>> Array (a, n) = "fun a b
+    -\<gtr\> Array.make a b"
+
+    external let array_get :
+
+    <math|\<forall\>>n, k, a [0<math|\<leqslant\>>k <math|\<wedge\>>
+    k+1<math|\<leqslant\>>n]. Array (a, n) <math|\<rightarrow\>> Num k
+    <math|\<rightarrow\>> a = "fun a b -\<gtr\> Array.get a b"
 
-    \ \ \ \ ematch l with
+    external let array_length :
 
-    \ \ \ \ \| Empty -\<gtr\> assert false
+    \ \ <math|\<forall\>>n, a [0<math|\<leqslant\>>n]. Array (a, n)
+    <math|\<rightarrow\>> Num n = "fun a -\<gtr\> Array.length a"
 
-    \ \ \ \ \| Node (ll, lx, lr, _) -\<gtr\>
+    datatype LinOrder
 
-    \ \ \ \ \ \ (ematch height ll, height lr with
+    datacons LE : LinOrder
 
-    \ \ \ \ \ \ \| m, n when n \<less\>= m -\<gtr\>
+    datacons GT : LinOrder
 
-    \ \ \ \ \ \ \ \ let r' = create lr x r in
+    datacons EQ : LinOrder
 
-    \ \ \ \ \ \ \ \ create ll lx r'
+    external let compare : <math|\<forall\>>a. a <math|\<rightarrow\>> a
+    <math|\<rightarrow\>> LinOrder =
 
-    \ \ \ \ \ \ \| m, n when m+1 \<less\>= n -\<gtr\>
+    \ \ "fun a b -\> let c = Pervasives.compare a b in
 
-    \ \ \ \ \ \ \ \ (ematch lr with
+    \ \ \ \ \ \ \ \ \ \ \ \ \ \ if c \< 0 then LE else if c \> 0 then GT else
+    EQ"
+
+    external let equal : <math|\<forall\>>a. a <math|\<rightarrow\>> a
+    <math|\<rightarrow\>> Bool = "fun a b -\<gtr\> a = b"
+
+    external let div2 : <math|\<forall\>>n. Num (2 n) <math|\<rightarrow\>>
+    Num n = "fun x -\<gtr\> x / 2"
+
+    \;
+
+    let bsearch key vec =
+
+    \ \ let rec look key vec lo hi =
+
+    \ \ \ \ eif lo \<= hi then
+
+    \ \ \ \ \ \ \ \ let m = div2 (hi + lo) in
+
+    \ \ \ \ \ \ \ \ let x = array_get vec m in
+
+    \ \ \ \ \ \ \ \ ematch compare key x with
+
+    \ \ \ \ \ \ \ \ \ \ \| LE -\> look key vec lo (m + (-1))
+
+    \ \ \ \ \ \ \ \ \ \ \| GT -\> look key vec (m + 1) hi
+
+    \ \ \ \ \ \ \ \ \ \ \| EQ -\> eif equal key x then m else -1
+
+    \ \ \ \ else -1 in
+
+    \ \ look key vec 0 (array_length vec + (-1))
+  </code>
+
+  \ We get the result type <verbatim|<math|\<exists\>>n[0 <math|\<leqslant\>>
+  n + 1].Num n> instead of <verbatim|<math|\<exists\>>k[k <math|\<leqslant\>>
+  n <math|\<wedge\>> 0 <math|\<leqslant\>> k + 1].Num k>. The inference of
+  the intended type succeeds after we introduce an appropriate assertion,
+  e.g. <verbatim|assert num -1 \<= hi>.
+
+  The example <verbatim|liquid_tower_harder.gadt> creates too complex an
+  abduction problem at a late iteration of the type inference problem.
+  Paradoxically, the example is harder than <verbatim|liquid_tower.gadt>,
+  despite the latter performing a joint inference of all the functions. The
+  <verbatim|liquid_tower.gadt> example leads to more parameter sharing and
+  thus easier abduction problems.
+
+  Examples <verbatim|liquid_simplex_step_3.gadt>,
+  <verbatim|liquid_simplex_step_4.gadt> and
+  <verbatim|liquid_gauss_rowMax.gadt> result in uninformative, empty
+  postconditions, because to tell more would require inspecting the behavior
+  of the respective function across recursive calls. To save space, we list
+  just the function definition from <verbatim|liquid_simplex_step_3.gadt>:
+
+  <\code>
+    let rec enter_var arr2 n j c j' =
 
-    \ \ \ \ \ \ \ \ \| Empty -\<gtr\> assert false
+    \ \ eif j' + 2 \<= n then
 
-    \ \ \ \ \ \ \ \ \| Node (lrl, lrx, lrr, _) -\<gtr\>
+    \ \ \ \ let c' = matrix_get arr2 0 j' in
 
-    \ \ \ \ \ \ \ \ \ \ let l' = create ll lx lrl in
+    \ \ \ \ eif less c' c then enter_var arr2 n j' c' (j'+1)
 
-    \ \ \ \ \ \ \ \ \ \ let r' = create lrr x r in
+    \ \ \ \ else enter_var arr2 n j c (j'+1)
 
-    \ \ \ \ \ \ \ \ \ \ create l' lrx r'))
+    \ \ else j
   </code>
 
-  Unfortunately, it seems it would require too much ``guesswork'' from the
-  inference algorithms.
+  Fortunately, if the function is used in the same toplevel definition in
+  which it is defined, use-site requirements facilitate the inference of the
+  intended postcondition.
+
+  The example <verbatim|liquid_gauss_harder.gadt> poses too big a challenge
+  for InvarGenT. To get the example <verbatim|liquid_gauss.gadt> that passes
+  inference, we needed to modify it in two ways. One was streamlining one of
+  the nested definitions, to not introduce another, unnecessary level of
+  nesting. The other was to relax the constraint on the processed portion of
+  the matrix, coming from the restriction on the matrix size intended in the
+  original source of the <verbatim|liquid_gauss_harder.gadt> example. In
+  <verbatim|liquid_gauss.gadt>, the whole matrix is processed and the
+  inferred type is most general.
 </body>
 
 <\initial>
diff --git a/examples/avl_delmin-simpler.gadt b/examples/avl_delmin_simpler.gadt
similarity index 100%
rename from examples/avl_delmin-simpler.gadt
rename to examples/avl_delmin_simpler.gadt
diff --git a/examples/avl_delmin-simpler.gadti.target b/examples/avl_delmin_simpler.gadti.target
similarity index 100%
rename from examples/avl_delmin-simpler.gadti.target
rename to examples/avl_delmin_simpler.gadti.target
diff --git a/examples/binary_plus-harder.gadt b/examples/binary_plus_harder.gadt
similarity index 100%
rename from examples/binary_plus-harder.gadt
rename to examples/binary_plus_harder.gadt
diff --git a/examples/binary_plus-harder.gadti.target b/examples/binary_plus_harder.gadti.target
similarity index 100%
rename from examples/binary_plus-harder.gadti.target
rename to examples/binary_plus_harder.gadti.target
diff --git a/examples/non_outsidein-rx.gadt b/examples/non_outsidein_rx.gadt
similarity index 100%
rename from examples/non_outsidein-rx.gadt
rename to examples/non_outsidein_rx.gadt
diff --git a/examples/non_outsidein-rx.gadti.target b/examples/non_outsidein_rx.gadti.target
similarity index 100%
rename from examples/non_outsidein-rx.gadti.target
rename to examples/non_outsidein_rx.gadti.target
diff --git a/examples/non_pointwise_avl_delmin-modified.gadt b/examples/non_pointwise_avl_delmin_modified.gadt
similarity index 100%
rename from examples/non_pointwise_avl_delmin-modified.gadt
rename to examples/non_pointwise_avl_delmin_modified.gadt
diff --git a/examples/non_pointwise_avl_delmin-modified.gadti.target b/examples/non_pointwise_avl_delmin_modified.gadti.target
similarity index 100%
rename from examples/non_pointwise_avl_delmin-modified.gadti.target
rename to examples/non_pointwise_avl_delmin_modified.gadti.target
diff --git a/examples/non_pointwise_fd_comp-harder.gadt b/examples/non_pointwise_fd_comp_harder.gadt
similarity index 100%
rename from examples/non_pointwise_fd_comp-harder.gadt
rename to examples/non_pointwise_fd_comp_harder.gadt
diff --git a/examples/non_pointwise_fd_comp-harder.gadti.target b/examples/non_pointwise_fd_comp_harder.gadti.target
similarity index 100%
rename from examples/non_pointwise_fd_comp-harder.gadti.target
rename to examples/non_pointwise_fd_comp_harder.gadti.target
diff --git a/examples/non_pointwise_zip1-modified.gadt b/examples/non_pointwise_zip1_modified.gadt
similarity index 100%
rename from examples/non_pointwise_zip1-modified.gadt
rename to examples/non_pointwise_zip1_modified.gadt
diff --git a/examples/non_pointwise_zip1-modified.gadti.target b/examples/non_pointwise_zip1_modified.gadti.target
similarity index 100%
rename from examples/non_pointwise_zip1-modified.gadti.target
rename to examples/non_pointwise_zip1_modified.gadti.target
diff --git a/examples/non_pointwise_zip1-simpler.gadt b/examples/non_pointwise_zip1_simpler.gadt
similarity index 100%
rename from examples/non_pointwise_zip1-simpler.gadt
rename to examples/non_pointwise_zip1_simpler.gadt
diff --git a/examples/non_pointwise_zip1-simpler.gadti.target b/examples/non_pointwise_zip1_simpler.gadti.target
similarity index 100%
rename from examples/non_pointwise_zip1-simpler.gadti.target
rename to examples/non_pointwise_zip1_simpler.gadti.target
diff --git a/examples/non_pointwise_zip1-simpler2.gadt b/examples/non_pointwise_zip1_simpler2.gadt
similarity index 100%
rename from examples/non_pointwise_zip1-simpler2.gadt
rename to examples/non_pointwise_zip1_simpler2.gadt
diff --git a/examples/non_pointwise_zip1-simpler2.gadti.target b/examples/non_pointwise_zip1_simpler2.gadti.target
similarity index 100%
rename from examples/non_pointwise_zip1-simpler2.gadti.target
rename to examples/non_pointwise_zip1_simpler2.gadti.target
diff --git a/examples/pointwise_zip2-harder.gadt b/examples/pointwise_zip2_harder.gadt
similarity index 100%
rename from examples/pointwise_zip2-harder.gadt
rename to examples/pointwise_zip2_harder.gadt
diff --git a/examples/pointwise_zip2-harder.gadti.target b/examples/pointwise_zip2_harder.gadti.target
similarity index 57%
rename from examples/pointwise_zip2-harder.gadti.target
rename to examples/pointwise_zip2_harder.gadti.target
index b5179b5..42134ea 100644
--- a/examples/pointwise_zip2-harder.gadti.target
+++ b/examples/pointwise_zip2_harder.gadti.target
@@ -1,10 +1,13 @@
 datatype List : type
+
 datacons N : ∀a. List a
-datacons C : ∀a. a * List a ⟶ List a
+
+datacons C : ∀a.a * List a ⟶ List a
 
 datatype Zip2 : type * type
+
 datacons Zero2 : ∀a. Zip2 (a, List a)
-datacons Succ2 :
-  ∀a, b, c. Zip2 (a, b) ⟶ Zip2 ((c → a), (List c → b))
+
+datacons Succ2 : ∀a, b, c.Zip2 (a, b) ⟶ Zip2 (c → a, List c → b)
 
 val zip2 : ∀a, b. Zip2 (a, b) → a → b
diff --git a/examples/pointwise_zip2-simpler1.gadt b/examples/pointwise_zip2_simpler1.gadt
similarity index 100%
rename from examples/pointwise_zip2-simpler1.gadt
rename to examples/pointwise_zip2_simpler1.gadt
diff --git a/examples/pointwise_zip2-simpler1.gadti.target b/examples/pointwise_zip2_simpler1.gadti.target
similarity index 100%
rename from examples/pointwise_zip2-simpler1.gadti.target
rename to examples/pointwise_zip2_simpler1.gadti.target
diff --git a/examples/pointwise_zip2-simpler2.gadt b/examples/pointwise_zip2_simpler2.gadt
similarity index 100%
rename from examples/pointwise_zip2-simpler2.gadt
rename to examples/pointwise_zip2_simpler2.gadt
diff --git a/examples/pointwise_zip2-simpler2.gadti.target b/examples/pointwise_zip2_simpler2.gadti.target
similarity index 100%
rename from examples/pointwise_zip2-simpler2.gadti.target
rename to examples/pointwise_zip2_simpler2.gadti.target
diff --git a/examples/pointwise_zip2-simpler3.gadt b/examples/pointwise_zip2_simpler3.gadt
similarity index 100%
rename from examples/pointwise_zip2-simpler3.gadt
rename to examples/pointwise_zip2_simpler3.gadt
diff --git a/examples/pointwise_zip2-simpler3.gadti.target b/examples/pointwise_zip2_simpler3.gadti.target
similarity index 100%
rename from examples/pointwise_zip2-simpler3.gadti.target
rename to examples/pointwise_zip2_simpler3.gadti.target
diff --git a/examples/pointwise_zip2-simpler4.gadt b/examples/pointwise_zip2_simpler4.gadt
similarity index 100%
rename from examples/pointwise_zip2-simpler4.gadt
rename to examples/pointwise_zip2_simpler4.gadt
diff --git a/examples/pointwise_zip2-simpler4.gadti.target b/examples/pointwise_zip2_simpler4.gadti.target
similarity index 100%
rename from examples/pointwise_zip2-simpler4.gadti.target
rename to examples/pointwise_zip2_simpler4.gadti.target
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
index c3a8e05..79a635a 100644
--- a/src/InvarGenTTest.ml
+++ b/src/InvarGenTTest.ml
@@ -17,7 +17,8 @@ let input_file file =
    with End_of_file -> ());
   Buffer.contents buf
 
-let test_case ?(test_annot=false) ?richer_answers ?more_general_num
+let test_case ?(test_annot=false) ?(do_ml=true)
+    ?richer_answers ?more_general_num
     ?prefer_guess ?prefer_bound_to_local ?prefer_bound_to_outer
     ?abd_rotations ?num_abd_timeout
     ?num_abd_fail_timeout ?nodeadcode file () =
@@ -76,7 +77,7 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
   (try
      let verif_res =
        (*[* Format.printf "test_case: file=%s@\n%!" file; *]*)
-       InvarGenT.process_file ~do_sig:true ~do_ml:true
+       InvarGenT.process_file ~do_sig:true ~do_ml
          ~full_annot:test_annot (file^".gadt") in
      assert_equal ~printer:(fun x->x)
        (input_file (file^".gadti.target"))
@@ -160,7 +161,7 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            todo "currently requiring expanded arguments";
            skip_if !debug "debug";
-           test_case "binary_plus-harder" ());
+           test_case "binary_plus_harder" ());
       "flatten_pairs" >::
         (fun () ->
            skip_if !debug "debug";
@@ -168,7 +169,7 @@ let tests = "InvarGenT" >::: [
       "flatten_quadrs" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~abd_rotations:4 "flatten_quadrs" ());
+           test_case "flatten_quadrs" ());
       "equational_reas" >::
         (fun () ->
            skip_if !debug "debug";
@@ -241,29 +242,27 @@ let tests = "InvarGenT" >::: [
       "pointwise-zip2-simpler1" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler1" ());
+           test_case "pointwise_zip2_simpler1" ());
       "pointwise-zip2-simpler2" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler2" ());
+           test_case "pointwise_zip2_simpler2" ());
       "pointwise-zip2-simpler3" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler3" ());
+           test_case "pointwise_zip2_simpler3" ());
       "pointwise-zip2-simpler4" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "pointwise_zip2-simpler4" ());
+           test_case "pointwise_zip2_simpler4" ());
       "pointwise-zip2" >::
         (fun () ->
-           (* This test is close enough. *)
            skip_if !debug "debug";
            test_case "pointwise_zip2" ());
       "pointwise-zip2-harder" >::
         (fun () ->
-           todo "too hard but not call-by-value";
            skip_if !debug "debug";
-           test_case "pointwise_zip2-harder" ());
+           test_case ~do_ml:false "pointwise_zip2_harder" ());
       "pointwise-avl_rotl" >::
         (fun () ->
            skip_if !debug "debug";
@@ -295,7 +294,7 @@ let tests = "InvarGenT" >::: [
       "non_outsidein-rx" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "non_outsidein-rx" ());
+           test_case "non_outsidein_rx" ());
       "non_pointwise-split" >::
         (fun () ->
            skip_if !debug "debug";
@@ -319,11 +318,11 @@ let tests = "InvarGenT" >::: [
       "avl_delmin-simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "avl_delmin-simpler" ());
+           test_case "avl_delmin_simpler" ());
       "non_pointwise-avl_delmin-modified" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case "non_pointwise_avl_delmin-modified" ());
+           test_case "non_pointwise_avl_delmin_modified" ());
       "non_pointwise-avl_delmin" >::
         (fun () ->
            skip_if !debug "debug";
@@ -344,19 +343,19 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            todo "currently requiring expanded arguments";
            skip_if !debug "debug";
-           test_case "non_pointwise_fd_comp-harder" ());
+           test_case "non_pointwise_fd_comp_harder" ());
       "non_pointwise-zip1-simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-simpler" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_simpler" ());
       "non_pointwise-zip1-simpler2" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-simpler2" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_simpler2" ());
       "non_pointwise-zip1-modified" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_guess:true "non_pointwise_zip1-modified" ());
+           test_case ~prefer_guess:true "non_pointwise_zip1_modified" ());
       "non_pointwise-zip1" >::
         (fun () ->
            skip_if !debug "debug";
@@ -377,16 +376,6 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            skip_if !debug "debug";
            test_case "avl_tree" ());
-      "binomial_heap-ins_tree" >::
-        (fun () ->
-           todo "TODO";
-           skip_if !debug "debug";
-           test_case "binomial_heap-ins_tree" ());
-      "binomial_heap-merge" >::
-        (fun () ->
-           todo "TODO";
-           skip_if !debug "debug";
-           test_case "binomial_heap-merge" ());
       "binomial_heap" >::
         (fun () ->
            todo "TODO";
@@ -468,7 +457,7 @@ let tests = "InvarGenT" >::: [
       "liquid_isort-simpler3" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~more_general_num:true "liquid_isort_simpler3" ());
+           test_case "liquid_isort_simpler3" ());
       "liquid_isort-simpler" >::
         (fun () ->
            skip_if !debug "debug";
@@ -567,7 +556,7 @@ let tests = "InvarGenT" >::: [
            test_case ~prefer_bound_to_local:true "liquid_simplex_step_3a" ());
       "liquid_simplex_step_4" >::
         (fun () ->
-           todo "FIXME"; (* "too hard for current InvarGenT"; ? *)
+           todo "too hard for current InvarGenT";
            skip_if !debug "debug";
            test_case "liquid_simplex_step_4" ());
       "liquid_simplex_step_4a" >::
@@ -637,7 +626,7 @@ let tests = "InvarGenT" >::: [
       "liquid_gauss_simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_bound_to_outer:true "liquid_gauss_simpler" ());
+           test_case "liquid_gauss_simpler" ());
       "liquid_gauss" >::
         (fun () ->
            skip_if !debug "debug";