Since the exact line of the construct that triggers VC may not be
known, the possibility to map the counterexample information related
to this construct to dedicated index instead of mapping it to line
number was added.

Note that the line of the construct that triggers VC is guaranteed to
be known only if  this construct does not span to multiple lines or if
the VC is not split.

the name of the projection to projected element.

Model elements in source code line are represented as list of JSON objects
with attributes "name", "value", and "kind". The attribute "name" is a
name of a counterexample element, the attribute "value" is the value of
the counterexample element, and the attribute "kind" is the kind of
counterexample element, currently one of "old", "result", "error_message",
and "other".

This fixes (-2) mod 2 being evaluated as nonzero.

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false

Issue: stack overflow when loading the driver, how can it be??

To do so, add "overriding" keyword in front of "syntax" in the driver file as in, e.g.,
  overriding syntax function to_uint "(bv2int %1)"

One can only have one overriding for a specific function/type.

Prevent loosing labels of formulas with f.t_node equal to Tquant in
transformations eliminate_algebraic and introduce_premises.

Need to compile Alt-Ergo with Nums instead of Zarith,
which is not supported by js_of_ocaml

The concatenation of strings in the list of strings returned by
bounded_split must be equal to the string being split.