search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
141 stars 61 forks source link

Simplify test fails with divide by zero (again). #620

Open philderbeast opened 2 years ago

philderbeast commented 2 years ago

Similar to #558 (which no longer fails), I saw a CI failure and it is reproducible: 

> cabal test tasty --test-options "--quickcheck-replay=85303 --quickcheck-max-size=4"
...
  simplify does not increase expression size
    PLE:                                       FAIL
      *** Failed! Exception: 'divide by zero' (after 379 tests and 3 shrinks):
      EBin Mod (ECon (I 0)) (ECon (I 0))
      Use --quickcheck-replay=85303 --quickcheck-max-size=4 to reproduce.
      Use -p '/PLE/' to rerun this test only.
    Interpreter:                               FAIL
      *** Failed! Exception: 'divide by zero' (after 379 tests and 3 shrinks):
      EBin Mod (ECon (I 0)) (ECon (I 0))
      Use --quickcheck-replay=85303 --quickcheck-max-size=4 to reproduce.
      Use -p '/Interpreter/' to rerun this test only.
  interpret
    computes a fixpoint:                       FAIL
      *** Failed! Exception: 'divide by zero' (after 379 tests and 3 shrinks):
      EBin Mod (ECon (I 0)) (ECon (I 0))
      Exception thrown while showing test case: 'divide by zero'
      Use --quickcheck-replay=85303 --quickcheck-max-size=4 to reproduce.
      Use -p '/computes a fixpoint/' to rerun this test only.