CVC4 suffered a segfault

cvc5 / cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

Other

1.05k stars 234 forks source link

CVC4 suffered a segfault #5441

Closed hernanponcedeleon closed 4 years ago

hernanponcedeleon commented 4 years ago

Describe the bug CVC4 suffered a segfault in the attached input. for_infinite_loop_1-O0.bpl.smt2.zip

Note: If the bug is triggered with an SMT2 input file please minimize it with ddsmt. The reducer did not managed to minimise the input (timeout after 5 min)

CVC4 version/commit: This is CVC4 version 1.7 compiled with GCC version 4.2.1 Compatible Apple LLVM 11.0.3 (clang-1103.0.32.62)

Operating system: MacOS 10.15.4

nafur commented 4 years ago

Seems to be a MacOS issue, can not reproduce on Linux (neither 1.7 nor current master).

Update: maybe you could try pydelta instead (pydelta --match-err "suffered a segfault" cvc4 input.smt2)

hernanponcedeleon commented 4 years ago

I build cvc4 from the master branch and it does not crash for the file I uploaded. I got many other similar crashes (in the master branch) but I was not able to reproduce any of them in Linux.