search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
817 stars 181 forks source link

Core dumped when enumerating solutions #772

Closed olegzaikin closed 2 weeks ago

olegzaikin commented 2 weeks ago

Version 5.11.22, the binary cryptominisat5 is taken from cryptominisat5-linux-amd64.zip On the CNF 1.cnf

p cnf 2 2 1 2 0 -1 2 0

and the run

./cryptominisat5 --maxsol 2 ./1.cnf

it crashes:

s SATISFIABLE v -1 2 0 c Number of solutions found until now: 1 terminate called after throwing an instance of 'std::runtime_error' what(): Sampling vars not set Aborted (core dumped)

The strange thing is that

./cryptominisat --version

gives '1.0'

P.S. On version 5.11.21 everything works fine.

capiman commented 2 weeks ago

Just wanted to add, that I can reproduce the version "1.0" on my system.

martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ ./cryptominisat5
c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 78c852ebc6816db9cdaa16a669eb3c2545587473
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 =  -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 = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . |
c CMS compiled with gcc version 13.2.0
c Executed with command line: ./cryptominisat5
c Reading from standard input... Use '-h' or '--help' for help.
^Cc
*** INTERRUPTED ***
No clauses or variables were put into the solver, exiting without stats
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ ./cryptominisat5 --version
1.0
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$

I just cloned the repos and started a completely new build. The version "1.0" is reported with --version, but when calling cryptominisat5 without any arguments, it tells:

c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 78c852ebc6816db9cdaa16a669eb3c2545587473
...
capiman commented 2 weeks ago

I can also reproduce the segfault:

martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ ./cryptominisat5 --maxsol 2 ./1.cnf
c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 78c852ebc6816db9cdaa16a669eb3c2545587473
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 =  -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 = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . |
c CMS compiled with gcc version 13.2.0
c Executed with command line: ./cryptominisat5 --maxsol 2 ./1.cnf
c Reading file './1.cnf'
c -- header says num vars:              2
c -- header says num clauses:           2
c WARNING: Empty line at line number 4 -- this is not part of the DIMACS specifications (http://www.satcompetition.org/2009/format-benchmarks2009.html). Ignoring.
c -- clauses added: 2
c -- xor clauses added: 0
c -- vars added 2
c Parsing time: 0.00 s
c [branch] adjusting to: vsid (from: vsid) var_decay:0.95 descr: VSIDS
c rst  geom  stb   vs     1     0       2     0     2    0.00    2.00     0     0     0     0    0.00    0.00
s SATISFIABLE
v -1 2 0
c Number of solutions found until now:      1
terminate called after throwing an instance of 'std::runtime_error'
  what():  Sampling vars not set
Aborted (core dumped)
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ gdb --args ./cryptominisat5 --maxsol 2 ./1.cnf
GNU gdb (Ubuntu 15.0.50.20240403-0ubuntu1) 15.0.50.20240403-git
Copyright (C) 2024 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./cryptominisat5...
(gdb) run
Starting program: /home/martin/testclone/cryptominisat/build/cryptominisat5 --maxsol 2 ./1.cnf

This GDB supports auto-downloading debuginfo from the following URLs:
  <https://debuginfod.ubuntu.com>
Enable debuginfod for this session? (y or [n]) y
Debuginfod has been enabled.
To make this setting permanent, add 'set debuginfod enabled on' to .gdbinit.
Downloading separate debug info for system-supplied DSO at 0x7ffff7fc3000
Downloading separate debug info for /lib/x86_64-linux-gnu/libz.so.1
Downloading separate debug info for /lib/x86_64-linux-gnu/libgmp.so.10
Downloading separate debug info for /lib/x86_64-linux-gnu/libstdc++.so.6
Downloading separate debug info for /lib/x86_64-linux-gnu/libgcc_s.so.1
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
Downloading separate debug info for /home/martin/testclone/cadiback/libcadiback.so
Downloading separate debug info for /home/martin/testclone/cadical/build/libcadical.so
c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 78c852ebc6816db9cdaa16a669eb3c2545587473
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 =  -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 = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . |
c CMS compiled with gcc version 13.2.0
c Executed with command line: /home/martin/testclone/cryptominisat/build/cryptominisat5 --maxsol 2 ./1.cnf
c Reading file './1.cnf'
c -- header says num vars:              2
c -- header says num clauses:           2
c WARNING: Empty line at line number 4 -- this is not part of the DIMACS specifications (http://www.satcompetition.org/2009/format-benchmarks2009.html). Ignoring.
c -- clauses added: 2
c -- xor clauses added: 0
c -- vars added 2
c Parsing time: 0.00 s
c [branch] adjusting to: vsid (from: vsid) var_decay:0.95 descr: VSIDS
c rst  geom  stb   vs     1     0       2     0     2    0.00    2.00     0     0     0     0    0.00    0.00
s SATISFIABLE
v -1 2 0
c Number of solutions found until now:      1
terminate called after throwing an instance of 'std::runtime_error'
  what():  Sampling vars not set

Program received signal SIGABRT, Aborted.
Download failed: Invalid argument.  Continuing without source file ./nptl/./nptl/pthread_kill.c.
__pthread_kill_implementation (no_tid=0, signo=6, threadid=<optimized out>) at ./nptl/pthread_kill.c:44
warning: 44     ./nptl/pthread_kill.c: No such file or directory
(gdb) bt
#0  __pthread_kill_implementation (no_tid=0, signo=6, threadid=<optimized out>) at ./nptl/pthread_kill.c:44
#1  __pthread_kill_internal (signo=6, threadid=<optimized out>) at ./nptl/pthread_kill.c:78
#2  __GI___pthread_kill (threadid=<optimized out>, signo=signo@entry=6) at ./nptl/pthread_kill.c:89
#3  0x00007ffff764526e in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#4  0x00007ffff76288ff in __GI_abort () at ./stdlib/abort.c:79
#5  0x00007ffff7aa5ffe in __gnu_cxx::__verbose_terminate_handler () at ../../../../src/libstdc++-v3/libsupc++/vterminate.cc:95
#6  0x00007ffff7abae9c in __cxxabiv1::__terminate (handler=<optimized out>) at ../../../../src/libstdc++-v3/libsupc++/eh_terminate.cc:48
#7  0x00007ffff7aa5a49 in std::terminate () at ../../../../src/libstdc++-v3/libsupc++/eh_terminate.cc:58
#8  0x00007ffff7abb128 in __cxxabiv1::__cxa_throw (obj=<optimized out>, tinfo=0x7ffff7c6deb8 <typeinfo for std::runtime_error>,
    dest=0x7ffff7ad0cb0 <std::runtime_error::~runtime_error()>) at ../../../../src/libstdc++-v3/libsupc++/eh_throw.cc:98
#9  0x00007ffff7e91aab in CMSat::SATSolver::get_sampl_vars (this=<optimized out>) at /home/martin/testclone/cryptominisat/src/cryptominisat.cpp:1877
#10 0x0000555555562cd5 in Main::ban_found_solution (this=this@entry=0x7fffffffd710) at /home/martin/testclone/cryptominisat/src/main.cpp:1377
#11 0x0000555555562f1b in Main::multi_solutions (this=this@entry=0x7fffffffd710) at /home/martin/testclone/cryptominisat/src/main.cpp:1360
#12 0x000055555556466d in Main::solve (this=this@entry=0x7fffffffd710) at /home/martin/testclone/cryptominisat/src/main.cpp:1299
#13 0x000055555555d1bc in main (argc=<optimized out>, argv=<optimized out>) at /home/martin/testclone/cryptominisat/src/main_exe.cpp:46
(gdb)
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ gcc --version
gcc (Ubuntu 13.2.0-23ubuntu4) 13.2.0
Copyright (C) 2023 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

martin@martin-ubuntu2024:~/testclone/cryptominisat/build$ uname -a
Linux martin-ubuntu2024 6.8.0-45-generic #45-Ubuntu SMP PREEMPT_DYNAMIC Fri Aug 30 12:02:04 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux
martin@martin-ubuntu2024:~/testclone/cryptominisat/build$
msoos commented 2 weeks ago

Wow! Nice catch!!! Sorry about that. It should now work. I'll do a new release for this and update this here :) Sorry about that.

capiman commented 2 weeks ago

I assume this is version

https://github.com/msoos/cryptominisat/blob/78c852ebc6816db9cdaa16a669eb3c2545587473/src/argparse.hpp#L1440

when using --version.

It is given back here

https://github.com/msoos/cryptominisat/blob/78c852ebc6816db9cdaa16a669eb3c2545587473/src/argparse.hpp#L1460

msoos commented 2 weeks ago

Thanks, version printing has been fixed too now :)