Crash when using Unigen Python bindings #9
Comments
|
Hi, Thanks for the bug report. I'd need a full backtrace -- can you please run this under Mate |
|
Hi Mate, Sure! Here's a link to the repo on the develop branch (https://github.com/UCSCFormalMethods/CIToolkit/tree/develop). I just pushed a commit that exhibits the bug consistently. You can set up the virtual environment by running At that point the test in question can be run with the command Eric |
|
Hi @msoos, I just wanted to check in and see if I can be of any more help debugging/resolving this. Thanks! |
|
Hey, Sorry for the late response. It was a bit overwhelming to set up an entire build environment, etc. to debug this. Can you please give me a backtrace? Thanks, Mate |
|
No problem! Hopefully this is what you're looking for, but if not please let me know. Thanks again for your help and please let me know how else I can help! |
|
Hi Mate, |
|
Hi Mate, |
|
Hi, I know I am incredibly late, but I have been having some personal issues. Sorry. Anyway. I spent today fixing up pycryptosat, it can now be built stand-alone. Not released yet, so now I wanna test with your tool :) I'm getting a build failure thanks to And then it all fails: I'll try to do something... though fixing numpy is really not my kind of thing :D Anyway, can you please check the code at: https://github.com/meelgroup/cryptominisat branch I'm using the latest Arch release, so that's why it's breaking, likely -- I have a new compiler, which warns more. Classic. |
|
Yay! I just managed to do everything. After fixing the above, I had an issue where my |
|
If you are happy with the above, I plan to release that CryptoMiniSat into the Mate |
|
Hi Mate, The best way to do that would be, inside the Thanks again! |
|
Hi, Here's my output: So it all seems good? Notice that I am using In other words it's: Where My python version is: I am running Arch Linux, gcc is: Do you know why I may not be getting the same error? Thanks for looking into this, Mate |
|
Hey Mate, I did a full reinstall of everything and it runs and passes all tests now, so I must have left some remnant of old code or been using an incorrect version. Sorry about the mixup and thanks so much for your help with all of this! Thanks again! |
|
Great to hear! Thanks for the bug report. I'll release the new CMS in a few
days :)
Mate
…On Fri, Jul 8, 2022, 23:53 Eric Vin ***@***.***> wrote:
Closed #9 <#9> as completed.
—
Reply to this email directly, view it on GitHub
<#9 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAKF4OIJX4EOND6Q62UZOYDVTCPOTANCNFSM5J74B6YA>
.
You are receiving this because you were mentioned.Message ID:
***@***.***>
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I've started using the Python bindings in my application and at the same time writing some tests that more vigorously test their usage. I've uncovered a situation where a CryptominiSat assert is failing. It only happens with certain formula/seed combinations as well. The assertion is:
cryptominisat/src/solver.cpp:4370: void CMSat::Solver::detach_xor_clauses(const std::set<unsigned int>&): Assertion seen[v] == 0 failed.and this is the code block it's referencing (Line 4370 in Solver.cpp):
//Clash on USED xorfor(auto& x: xorclauses) {x.detached = true;for(const uint32_t v: x.clash_vars) {assert(seen[v] == 0);seen[v] = 2;}}I can't seem to reproduce this on the command line interface, which might be because it does the counting first, but I think it's more likely I've done something wrong in the Python bindings. Do you have any insight as to what this issue is? My instinct is that I'm not setting something up correctly when I bypass the ApproxMC counting process.
I'm also more than happy to provide info on how to reproduce the bug using my tests if you're interested!
The text was updated successfully, but these errors were encountered: