runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
208 stars 41 forks source link

The simplification property test crashes (again). #1684

Closed mcalancea closed 2 years ago

mcalancea commented 4 years ago

Today I've had a test fail that was unrelated to my work. It can be reproduced with:

stack test --test-arguments "--hedgehog-replay \"Size 79 Seed 11061009888786495411 89260594792354819\""

Output:

` ✗ simplify returns simplified pattern failed at test/Test/SMT.hs:31:24 after 1 test.

                 ┏━━ test/Test/SMT.hs ━━━
              25 ┃ testPropertyWithSolver
              26 ┃     :: HasCallStack
              27 ┃     => String
              28 ┃     -> PropertyT SMT ()
              29 ┃     -> TestTree
              30 ┃ testPropertyWithSolver str =
              31 ┃     testProperty str . Hedgehog.property . Morph.hoist runSMT
                 ┃     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                 ┃     │ ━━━ Exception (ErrorCall) ━━━
                 ┃     │ Quantifying both the term and the predicate probably means that there's
                 ┃     │ an error somewhere else.
                 ┃     │ variable=Nl:intSort{}
                 ┃     │ patt=\and{intSort{}}(
                 ┃     │     /* term: */
                 ┃     │     /* Fn Sfa */ fInt{}(/* Fl Fn D Sfa */ Nl:intSort{}),
                 ┃     │ \and{intSort{}}(
                 ┃     │     /* predicate: */
                 ┃     │     /* Sfa */
                 ┃     │     \equals{intSort{}, intSort{}}(
                 ┃     │         /* Fl Fn D Sfa */ Nl:intSort{},
                 ┃     │         /* Fn Sfa */ fInt{}(/* Fl Fn D Sfa */ Nl:intSort{})
                 ┃     │     ),
                 ┃     │     /* substitution: */
                 ┃     │     \top{intSort{}}()
                 ┃     │ ))
                 ┃     │ 
                 ┃     │ CallStack (from HasCallStack):
                 ┃     │   error, called at src/Kore/Step/Simplification/Exists.hs:409:6 in kore-0.0.1.0-KGASRH7yiuGDe7eEfb8Hiq:Kore.Step.Simplification.Exists

              This failure can be reproduced by running:
              > recheck (Size 79) (Seed 11061009888786495411 89260594792354819) simplify returns simplified pattern

          Use '--hedgehog-replay "Size 79 Seed 11061009888786495411 89260594792354819"' to reproduce.

`

It seems the same test has failed in the past: https://github.com/kframework/kore/issues/1342.

Later Edit: Also here https://github.com/kframework/kore/issues/1467.

virgil-serbanuta commented 4 years ago

Last time it was a problem with how we were generating tests, but we should make sure it's not a problem with the simplification code.