grisette 0.12.0.0

[alexeyzab]

                 RoundingOp:
                   fpRoundingUnaryOp:
                     fp.roundToIntegral: [Failed]
           *** Failed! Exception: 'HUnitFailure (Just (SrcLoc {srcLocPackage = "grisette-0.12.0.0-FVKYylAMm4jEZGYKjAGKmD-spec", srcLocModule = "Grisette.Backend.TermRewritingTests", srcLocFile = "test/Grisette/Backend/TermRewritingTests.hs", srcLocStartLine = 183, srcLocStartCol = 7,
 srcLocEndLine = 183, srcLocEndCol = 20})) (Reason "Bad rewriting with unsolvable formula: (fp.roundToIntegral rtn a) was rewritten to (fp.roundToIntegral rtn a) under preconditiontrue corresponding same formula:(|| (&& (is_nan (fp.roundToIntegral rtn a)) (is_nan (fp.roundToIntegral
rtn a))) (= (fp.roundToIntegral rtn a) (fp.roundToIntegral rtn a)))")' (after 42 tests):
           FPRoundingModeSpec { no: rtn, re: rtn }
           IEEEFPSpec { no: a, re: a }
           (used seed -4253813048176111661)

cc @lsrcz

[lsrcz]

Hi @alexeyzab,

Thanks for reporting this. Unfortunately, I cannot reproduce this test failure. The error seems to originate from either an unknown result from Z3 or a solver crash, but I didn't see this happening when I was trying to isolate the case and run it locally.

I tested with the same binary as in Stackage CI, and it runs without crashing. I also haven't seen this in Grisette's CI.

Is it possible that something external, like an OOM killer, might have caused the failure?