Tests that crash don't print counterexamples
Opened this issue · 1 comments
byorgey commented
Consider this test (from test/prop-fail/
):
!!! forall a : Q, b : Q. divide a b * b =!= a
divide : Q -> Q -> Q
divide a b = a / b
It fails with a division by zero error, as it should, and prints out an example that led to the crash (a = 0, b = 0
). After merging #365 , however, it will still fail but no longer prints out the example. Splitting out a separate issue to look into this later.
byorgey commented
For reference, here's the current output:
Disco> :load test/prop-fail/bad-tests.disco
Loading bad-tests.disco...
Running tests...
badmap:
- Certainly false: badmap(λx. x / 0)([3, 4, 5]) =!= [6, 7, 8]
Test failed with an error:
Error: division by zero.
- Certainly false: badmap(λx. x)([1, 2]) =!= [1, 2]
- Left side: [1, 1, 2, 2, 3]
- Right side: [1, 2]
- Certainly false: badmap(λx. x + 1)([3, 4]) > [5, 6]
divide:
- Certainly false: ∀a, b. divide(a)(b) * b =!= a
Test failed with an error:
Error: division by zero.
- Certainly false: ∀a. divide(a)(2) < a
Found counterexample:
a = 0
- Possibly false: ∃a. divide(a)(2) =!= abs(a) + 1
No example was found; checked 50 possibilities.
Loaded.