Incorrect equations when size limit is increased.

[rudymatela]

@barrucadu reports an issue when applying Speculate to DejaFu:

• speculate -t20000 -s5: doesn't find any equalities, only conditional equations.

• speculate -t20000 -s6: finds these equalities:

                          isBlock ta == isBlock ta'
    (isBarrier a == isCommit a crid) == (False == synchronises a crid)
  

  (isBarrier a == synchronises a crid) == (False == isCommit a crid) ...

Property 1 is wrong. Something gets weird with ThreadActions ("ta") when the size is increased, even though the number of tests remains the same.

[rudymatela]

I haven't looked into this in depth yet. But, as I mentioned to @barrucadu in person, the issue is most likely that an incorrect equation of bigger size was found then rewritten to an equation of smaller size. (The bigger the size of an equation, the larger the number of tests we need to falsify it). This causes the confusing behaviour of having an otherwise unfound equation of smaller size when size limit is increased.

To avoid this happening, before reporting equations, maybe Speculate should test them again with either the set number of tests or a separate larger number of tests. Perhaps also report a warning to the user that the number of tests should be increased as an incorrect equation was found.