Assertion 'false' failed on CMSat::findWatchedOfBin

[dampers]

Hi,

I'm trying to cryptanalysis with cryptominisat. and I got an error like this. [https://github.com/msoos/cryptominisat/issues/730] (and I ran 80 threads too.) So I recompile with-DLARGEMEM=ON option. (Thanks.) Unfortunately, I got this error...

cryptominisat-5.11.21/src/watchalgos.h:160: CMSat::Watched& CMSat::findWatchedOfBin(CMSat::watch_array&, CMSat::Lit, CMSat::Lit, bool, int32_t): Assertion 'false' failed.

version of cryptominisat c CryptoMiniSat version 5.11.21 c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file c CMS SHA revision GIT-notfound c Using VMTF code by Armin Biere from CaDiCaL c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14 c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96, c CMS is MIT licensed c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way' c by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]' c by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015 c CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -fvisibility=hidden -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES = -DLARGE_OFFSETS -DRDB0_ONLY_FEATURES -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = | STATS = OFF | SQLITE3_FOUND = | ZLIB_FOUND = TRUE | VALGRIND_FOUND = | ENABLE_TESTING = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = | PYTHON_LIBRARY = | PYTHON_INCLUDE_DIRS = | MY_TARGETS = | LARGEMEM = ON | LIMITMEM = OFF | BREAKID_LIBRARIES = | BREAKID-VER = . | BOSPHORUS_LIBRARIES = | BOSPH-VER = . | compilation date time = Jun 25 2024 10:50:24 c CMS compiled with gcc version 11.4.0

how can i handdle this error?

[msoos]

Wow, I'm sorry, I'll try to fuzz-test CryptoMiniSat and see if I can find this bug. Unfortunately, it's not easy to figure out what the bug is from your description. It likely is a bug that manifests itself in different ways, so I need to find a small problem where I can debug and fix it. Please give me a bit of time, I'll run some fuzzing overnight and hopefully catch this bug!

[dampers]

@msoos Thank you for your response! While trying to find a solution, I found an issue that got the same error I got. https://github.com/stp/stp/issues/471

[msoos]

This has now been fixed. Sorry for the delay.

[dampers]

Thank you for your prompt response and fix @msoos !