Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tests that crash don't print counterexamples #364

Open
byorgey opened this issue May 24, 2023 · 2 comments
Open

Tests that crash don't print counterexamples #364

byorgey opened this issue May 24, 2023 · 2 comments
Labels
C-Moderate Effort Should take a moderate amount of time to address. S-Nice to have Minor importance U-Testing

Comments

@byorgey
Copy link
Member

byorgey commented May 24, 2023

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 byorgey added C-Moderate Effort Should take a moderate amount of time to address. U-Testing S-Nice to have Minor importance labels May 24, 2023
@byorgey byorgey changed the title Tests that fail don't print counterexamples Tests that crash don't print counterexamples May 24, 2023
@byorgey
Copy link
Member Author

byorgey commented Mar 29, 2024

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.

@byorgey
Copy link
Member Author

byorgey commented Oct 14, 2024

Also, why does the - Certainly false: badmap(λx. x + 1)([3, 4]) > [5, 6] case not print out any counterexample either?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-Moderate Effort Should take a moderate amount of time to address. S-Nice to have Minor importance U-Testing
Projects
None yet
Development

No branches or pull requests

1 participant