Assertion `val2 == l_True' failed.

Mate,

With this model, I get the following output on a7052c4415965ce65f273a7fd2d88508ac1fcf05. Core dump here. This appears not to happen on the latest master (2a247e83c50a9217c23ee83b57e558d2f84876c4).

cryptominisat5: /home/cipherboy/cms/cms-git/src/solver.cpp:2677: void CMSat::Solver::check_implicit_propagated() const: Assertion `val2 == l_True' failed.

Program received signal SIGABRT, Aborted.
__GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:51
51  ../sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) backtrace
#0  __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:51
#1  0x00007ffff67a6f5d in __GI_abort () at abort.c:90
#2  0x00007ffff679cf17 in __assert_fail_base (fmt=<optimized out>, assertion=assertion@entry=0x7ffff7bbadda "val2 == l_True", file=file@entry=0x7ffff7bb9e18 "/home/cipherboy/cms/cms-git/src/solver.cpp", 
    line=line@entry=2677, function=function@entry=0x7ffff7bbb9e0 <CMSat::Solver::check_implicit_propagated() const::__PRETTY_FUNCTION__> "void CMSat::Solver::check_implicit_propagated() const") at assert.c:92
#3  0x00007ffff679cfc2 in __GI___assert_fail (assertion=assertion@entry=0x7ffff7bbadda "val2 == l_True", file=file@entry=0x7ffff7bb9e18 "/home/cipherboy/cms/cms-git/src/solver.cpp", line=line@entry=2677, 
    function=function@entry=0x7ffff7bbb9e0 <CMSat::Solver::check_implicit_propagated() const::__PRETTY_FUNCTION__> "void CMSat::Solver::check_implicit_propagated() const") at assert.c:101
#4  0x00007ffff7b61c35 in CMSat::Solver::check_implicit_propagated (this=<optimized out>) at /home/cipherboy/cms/cms-git/src/solver.cpp:2677
#5  0x00007ffff7b2a803 in CMSat::OccSimplifier::finishUp (this=this@entry=0x5555557ff7c0, origTrailSize=origTrailSize@entry=839) at /home/cipherboy/cms/cms-git/src/occsimplifier.cpp:1617
#6  0x00007ffff7b32c1d in CMSat::OccSimplifier::simplify (this=this@entry=0x5555557ff7c0, _startup=_startup@entry=false, schedule="occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-xor,")
    at /home/cipherboy/cms/cms-git/src/occsimplifier.cpp:1355
#7  0x00007ffff7b69c14 in CMSat::Solver::execute_inprocess_strategy (this=this@entry=0x5555557f8c10, startup=startup@entry=false, 
    strategy="handle-comps,scc-vrepl, cache-clean, cache-tryboth,sub-impl, intree-probe, probe,sub-str-cls-with-bin, distill-cls,scc-vrepl, sub-impl, str-impl, sub-impl,occ-backw-sub-str, occ-clean-implicit, occ-bv"...) at /home/cipherboy/cms/cms-git/src/solver.cpp:1683
#8  0x00007ffff7b6acd9 in CMSat::Solver::simplify_problem (this=this@entry=0x5555557f8c10, startup=startup@entry=false) at /home/cipherboy/cms/cms-git/src/solver.cpp:1851
#9  0x00007ffff7b6b0da in CMSat::Solver::iterate_until_solved (this=this@entry=0x5555557f8c10) at /home/cipherboy/cms/cms-git/src/solver.cpp:1578
#10 0x00007ffff7b6ce53 in CMSat::Solver::solve_with_assumptions (this=0x5555557f8c10, _assumptions=_assumptions@entry=0x0) at /home/cipherboy/cms/cms-git/src/solver.cpp:1325
#11 0x00007ffff7bae13f in calc (assumptions=assumptions@entry=0x0, solve=solve@entry=true, data=0x5555557f8b50) at /home/cipherboy/cms/cms-git/src/cryptominisat.cpp:645
#12 0x00007ffff7bae3fd in CMSat::SATSolver::solve (this=<optimized out>, assumptions=assumptions@entry=0x0) at /home/cipherboy/cms/cms-git/src/cryptominisat.cpp:684
#13 0x00005555555620f3 in Main::multi_solutions (this=this@entry=0x7fffffffdac0) at /home/cipherboy/cms/cms-git/src/main.cpp:1185
#14 0x00005555555652ee in Main::solve (this=0x7fffffffdac0) at /home/cipherboy/cms/cms-git/src/main.cpp:1159
#15 0x0000555555560f79 in main (argc=2, argv=0x7fffffffe4c8) at /home/cipherboy/cms/cms-git/src/main_exe.cpp:46

Not sure if this'll impact master on other models or if its been fixed, hence why I'm reporting it :) If you want me to test on other commits (git bisect?), I'd be happy to do that as well.

-- Alex

msoos / cryptominisat

Assertion `val2 == l_True' failed. #480