SmartCheck
SmartCheck copied to clipboard
Wrong generalization for the overflow example (PaperExample1)
This is perhaps related to issue #12.
For the motivating example of the SmartCheck paper, SmartCheck reports a correct counter-example, but an incorrect generalization:
forall values x0 x1 x2 x3:
T x3 (: -21874 x0) x2 (: -12585 []) x1
It is too general and includes values that are not counter-examples:
> let x0 = [21874]; x1 = []; x2 = []; x3 = []
> prop (T x3 (-21874:x0) x2 (-12585:[]) x1)
True
I have run the example with the default parameters, maybe tuning it to test more could fix this.