CryptoMiniSat assertion error

asked 2015-06-06 11:21:20 -0500

frollo gravatar image

I'm trying to use sage.sat.boolean_polynomials to solve a system of equations for my thesis. I'm ok with the fact it uses CryptoMiniSat as default but every time I run my script I get this error:

 Traceback (most recent call last):
  File "", line 104, in <module>
    s = alg_attack(p,c)
  File "", line 55, in alg_attack
    return solve_sat(F)
  File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/", line 179, in solve
    phi = converter(F)
  File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/", line 581, in __call__
  File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/", line 538, in clauses
  File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/", line 296, in clauses_sparse
  File "sage/sat/solvers/cryptominisat/cryptominisat.pyx", line 205, in sage.sat.solvers.cryptominisat.cryptominisat.CryptoMiniSat.add_clause (build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp:1672)

I got to line 205 of sage/sat/solvers/cryptominisat/cryptominisat.pyx and found this:


I found nothing about this in the documentation, so I decided to try some bad practices and commented away the assertion, restarted sage and tried again. I got the same error, referring to a line that is now a comment. I tried to restart my shell but, again, I got the same error.

Has anyone a clue about which could be causing this (the same script worked during the tests, the error just started showing up when I tried to run something serious)

edit retag flag offensive close merge delete


changing the code will only be taken into account if you do sage -br to re-build sage

FrédéricC gravatar imageFrédéricC ( 2015-06-06 14:32:08 -0500 )edit