The math used by the prover is different from C maths, so you may see some expressions that are neither part of standard C nor part of the eCv specification extensions. Here is a list of [some of] them. You should not see these in error messages, or anywhere else other than in proof/unproven output files - let us know if you do.
These are round-towards-zero versions of the / and % integer operators. Plain / and % in proofs refer to the version of integer division that always rounds down and the version of modulo that yields a result having the same sign as the divisor.
This means the number of elements in the collection operand. For an array arr, #arr equates to arr.count.
A variable of the form foo543,21 means the value of variable foo at line 543 column 21 in the .i file that was generated by the preprocessor. Similarly, heap543,21 means the value of the heap at that location.
The expression p.$r.value where p is a simple pointer is the prover's internal representation of *p. The expression ap.$r.value where ap is an array pointer is the prover's internal representation of ap.all, i.e. all the elements in the array to which ap points.
eCv Manual, Version 6.0, December 2012.
© 2012 Escher Technologies Limited. All rights reserved.