Investigate test failure in "computes a fixpoint"

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types

BSD 3-Clause "New" or "Revised" License

132 stars 60 forks source link

Investigate test failure in "computes a fixpoint" #657

Closed facundominguez closed 9 months ago

facundominguez commented 11 months ago

Investigate quickcheck failure in tasty testsuite at 75534d1. Noted in this job.

Tests
  ...
  interpret
    computes a fixpoint:                       FAIL
      *** Failed! Falsified (after 322 tests):
      EBin Div (ECon (R 0.0)) (ECon (I 0))
      ECon (R NaN) /= ECon (R NaN)
      Use --quickcheck-replay=241494 --quickcheck-max-size=4 to reproduce.
      Use -p '/computes a fixpoint/' to rerun this test only.