BUG: correct fingerprinting of variables

Variables were fingerprinted as `VAR(i)` where `i` an index,
and bound identifiers also with `VAR(j)` where `j` an index
produced using a different counter. The counter for variables
is `counthyp`, and the counter for bound constants and bound
variables is `countvar`.

When the two counters are both equal to 1,
`VAR(1)` results for both the occurrence of a variable, and
the occurrence of a constant bound by a rigid quantifier.

This commit adds a test file that catches this error.

src/backend/fingerprints.ml

@@ -246,10 +246,10 @@ let rec fp_expr counthyp countvar stack buf e =
            incr counthyp
        | Identvar s ->
            Stack.set stack n (Identvari !countvar,r);
-           bprintf buf "$VAR(%d)" !countvar;
+           bprintf buf "$PRM(%d)" !countvar;
            incr countvar
        | Identhypi i -> bprintf buf "$HYP(%d)" i
-       | Identvari i -> bprintf buf "$VAR(%d)" i
+       | Identvari i -> bprintf buf "$PRM(%d)" i
        | IdentBPragma -> ()
        end
     | Opaque s -> Buffer.add_string buf s

test/fast/fingerprint/FingerprintVariablesParameters_test.tla

@@ -0,0 +1,25 @@
+---- MODULE FingerprintVariablesParameters_test ----
+(* Test to ensure there is no coincidence between
+how variables and bound constants are fingerprinted.
+
+When this was a bug, the first run of TLAPM
+did not prove the second theorem below,
+but the assertions of the two theorems had identical
+fingerprints, so the second run of TLAPM proved
+both theorems. The commands for the test harness
+check this, by running TLAPM twice.
+*)
+
+VARIABLE x
+
+THEOREM \E y:  y # x
+OBVIOUS
+
+THEOREM \E y:  y # y
+OBVIOUS
+
+====================================
+command: ${TLAPM} --toolbox 0 0 ${FILE}
+stderr: 1/2 obligations failed
+command: ${TLAPM} --toolbox 0 0 ${FILE}
+stderr: 1/2 obligations failed