Help interpreting this error

[rithik-raja]

When I use a Map reduce in my parallelReduce invariant, I get an error that I can't seem to make sense of.

Verification failed:
  when ALL participants are honest
  of theorem: while invariant after loop
  at ./index.rsh:43:7:invariant

  // Violation Witness

  const UInt.max = 2000000;

  const v664 = <function return>;
  //    ^ could = false
  //      from: ./index.rsh:51:42:?:

  // Theorem Formalization

  assert(v664);

This seems to happen when I do something like sumOfVars == vars.sum() in the invariant.

The way I update each is vars[this] = fromSome(vars[this], 0) + increment
and the corresponding return statement is return [..., sumOfVars + increment, ...]

So assuming my logic is correct, what is going wrong?

[jeapostrophe]

What is line 51 in your program?

[rithik-raja]

I have DMed you on Discord with the code in question. The problem is map reduce in the invariant, particularly .sum() is giving me trouble. Sorry for the inconvenience.