SmartCheck icon indicating copy to clipboard operation
SmartCheck copied to clipboard

Wrong generalization for the overflow example (PaperExample1)

Open rudymatela opened this issue 8 years ago • 0 comments

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.

rudymatela avatar Aug 04 '17 14:08 rudymatela