search

ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

crash using ddsmt #30

Closed barrettcw closed 3 years ago

barrettcw commented 3 years ago

The attached file crashes when run with ddsmt t.smt2 out.smt2 cvc5

t.smt2.txt

barrettcw commented 3 years ago

OK - my mistake - it doesn't crash, but it produces a long list of backtraces Possibly a MacOS issue?

nafur commented 3 years ago

The backtrace is

File "/Library/Python/3.8/site-packages/ddsmt/strategy_hierarchical.py", line 182, in check
res = checker.check_exprs(exprs)
File "/Library/Python/3.8/site-packages/ddsmt/checker.py", line 139, in check_exprs
tmpfile = tmpfiles.get_tmp_filename()
File "/Library/Python/3.8/site-packages/ddsmt/tmpfiles.py", line 64, in get_tmp_filename
__TMPDIR.name,

but apparently no actual error is printed.

mpreiner commented 3 years ago

This was fixed by https://github.com/ddsmt/ddSMT/commit/9a04abb753df1859b053ebdbfe5cf2efc42e62d9

I just uploaded a new release to pypi, which includes this fix. @barrettcw can you try with version 2.0.2?

BrunoDutertre commented 3 years ago

This MacOS fix does not work for me. It doesn't look like it's included when one installs via

pip install ddsmt

I'm using python 3.9 on MacOS 11.5. The ddsmt shell script created by pip install is not the same as the bin/bbsmt in the repo.

Also, the python doc https://docs.python.org/3/library/multiprocessing.html?highlight=spawn seems to indicate that 'fork` is not safe on recent MacOS.

mpreiner commented 3 years ago

@BrunoDutertre Thanks for bringing this up. You're right the bin/ddsmt script is not the one that is used when installing with pip. pip generates its own script and calls the entrypoint of ddsmt from __main__.py. Another issue is fork on macOS, I didn't know about this issue. We'll have to find a fix for that. In the meanwhile can you checkout the ddsmt repo and use the bin/ddsmt instead?

BrunoDutertre commented 3 years ago

@mpreiner, Thanks. I've been using the repo version. It seems to be working fine so far.