search

vegard / sha1-sat

SAT instance generator for SHA-1
GNU General Public License v3.0
46 stars 14 forks source link

GIves runtime errors but runs without espresso #3

Closed msoos closed 6 years ago

msoos commented 11 years ago

$ ./sha1-gen --cnf > /dev/null terminate called after throwing an instance of 'std::runtime_error' what(): execve() failed terminate called after throwing an instance of 'std::runtime_error' what(): execve() failed terminate called after throwing an instance of 'std::runtime_error' what(): execve() failed terminate called after throwing an instance of 'std::runtime_error' what(): execve() failed terminate called after throwing an instance of 'std::runtime_error' what(): execve() failed

Is this OK? It gives a CNF, but I am not sure it's the best CNF? It's a bit confusing :(

solimul commented 6 years ago

These errors are thrown because sha-1-gen does not find the espresso executable (called from Line 220 of Main.cc). This is because the instruction given to setup the PATH for espresso does not work. With these errors, sha1-gen generates wrong CNFs, which are trivially solved by MiniSAT.

A duct-tape fix: 1) Modify Line 220 of sha1-sat-master/Main.cc and put the path for espresso executable as the first parameter of execlp function. Eg. execlp("../espresso", "espresso", 0) 2) Rebuild sha1-sat with "bash make.sh".

msoos commented 6 years ago

Ah, thanks, I'm closing this issue :) I have fixed this a long time ago :) I have my own fork of this repo :)